map_range (and map_index) combinator
authorhaftmann
Thu Oct 22 13:48:06 2009 +0200 (2009-10-22)
changeset 330634d462963a7db
parent 33062 542b34b178ec
child 33064 ba7ff3f9527a
map_range (and map_index) combinator
src/FOLP/simp.ML
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/SizeChange/sct.ML
src/HOL/String.thy
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Function/induction_scheme.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Function/scnp_solve.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/record.ML
src/HOL/Tools/refute.ML
src/Provers/order.ML
src/Provers/quasi.ML
src/Provers/trancl.ML
src/Pure/Syntax/parser.ML
src/Pure/library.ML
src/Pure/term.ML
src/Pure/unify.ML
src/Tools/Code/code_preproc.ML
     1.1 --- a/src/FOLP/simp.ML	Thu Oct 22 10:52:07 2009 +0200
     1.2 +++ b/src/FOLP/simp.ML	Thu Oct 22 13:48:06 2009 +0200
     1.3 @@ -534,7 +534,7 @@
     1.4  
     1.5  fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
     1.6  let fun xn_list(x,n) =
     1.7 -        let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
     1.8 +        let val ixs = map_range (fn i => (x^(radixstring(26,"a",i)),0)) (n - 1);
     1.9          in ListPair.map eta_Var (ixs, Library.take(n+1,Ts)) end
    1.10      val lhs = list_comb(f,xn_list("X",k-1))
    1.11      val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
     2.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Thu Oct 22 10:52:07 2009 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Oct 22 13:48:06 2009 +0200
     2.3 @@ -2035,8 +2035,8 @@
     2.4      val t = Thm.term_of ct;
     2.5      val fs = OldTerm.term_frees t;
     2.6      val bs = term_bools [] t;
     2.7 -    val vs = fs ~~ (0 upto (length fs - 1))
     2.8 -    val ps = bs ~~ (0 upto (length bs - 1))
     2.9 +    val vs = map_index swap fs;
    2.10 +    val ps = map_index swap bs;
    2.11      val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
    2.12    in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
    2.13  end;
     3.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Oct 22 10:52:07 2009 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Oct 22 13:48:06 2009 +0200
     3.3 @@ -2073,7 +2073,7 @@
     3.4      val thy = Thm.theory_of_cterm ct;
     3.5      val t = Thm.term_of ct;
     3.6      val fs = OldTerm.term_frees t;
     3.7 -    val vs = fs ~~ (0 upto (length fs - 1));
     3.8 +    val vs = map_index swap fs;
     3.9      val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t))));
    3.10    in Thm.cterm_of thy res end
    3.11  end;
     4.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Oct 22 10:52:07 2009 +0200
     4.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Oct 22 13:48:06 2009 +0200
     4.3 @@ -5898,7 +5898,7 @@
     4.4      val thy = Thm.theory_of_cterm ct;
     4.5      val t = Thm.term_of ct;
     4.6      val fs = OldTerm.term_frees t;
     4.7 -    val vs = fs ~~ (0 upto (length fs - 1));
     4.8 +    val vs = map_index swap fs;
     4.9      val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
    4.10      val t' = (term_of_fm vs o qe o fm_of_term vs) t;
    4.11    in (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
     5.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Oct 22 10:52:07 2009 +0200
     5.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Oct 22 13:48:06 2009 +0200
     5.3 @@ -965,8 +965,8 @@
     5.4   else if d = 0 then [FuncUtil.Ctermfunc.empty]
     5.5   else if null vars then [monomial_1] else
     5.6   let val alts =
     5.7 -  map (fn k => let val oths = enumerate_monomials (d - k) (tl vars)
     5.8 -               in map (fn ks => if k = 0 then ks else FuncUtil.Ctermfunc.update (hd vars, k) ks) oths end) (0 upto d)
     5.9 +  map_range (fn k => let val oths = enumerate_monomials (d - k) (tl vars)
    5.10 +               in map (fn ks => if k = 0 then ks else FuncUtil.Ctermfunc.update (hd vars, k) ks) oths end) (d + 1)
    5.11   in flat alts
    5.12   end;
    5.13  
    5.14 @@ -1202,9 +1202,9 @@
    5.15     val eq0 = map (poly_of_term o Thm.dest_arg1 o concl) eqs
    5.16     val le0 = map (poly_of_term o Thm.dest_arg o concl) les
    5.17     val lt0 = map (poly_of_term o Thm.dest_arg o concl) lts
    5.18 -   val eqp0 = map (fn (t,i) => (t,RealArith.Axiom_eq i)) (eq0 ~~ (0 upto (length eq0 - 1)))
    5.19 -   val lep0 = map (fn (t,i) => (t,RealArith.Axiom_le i)) (le0 ~~ (0 upto (length le0 - 1)))
    5.20 -   val ltp0 = map (fn (t,i) => (t,RealArith.Axiom_lt i)) (lt0 ~~ (0 upto (length lt0 - 1)))
    5.21 +   val eqp0 = map_index (fn (i, t) => (t,RealArith.Axiom_eq i)) eq0
    5.22 +   val lep0 = map_index (fn (i, t) => (t,RealArith.Axiom_le i)) le0
    5.23 +   val ltp0 = map_index (fn (i, t) => (t,RealArith.Axiom_lt i)) lt0
    5.24     val (keq,eq) = List.partition (fn (p,_) => multidegree p = 0) eqp0
    5.25     val (klep,lep) = List.partition (fn (p,_) => multidegree p = 0) lep0
    5.26     val (kltp,ltp) = List.partition (fn (p,_) => multidegree p = 0) ltp0
     6.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Oct 22 10:52:07 2009 +0200
     6.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Oct 22 13:48:06 2009 +0200
     6.3 @@ -643,9 +643,9 @@
     6.4  
     6.5    fun linear_prover (eq,le,lt) = 
     6.6     let 
     6.7 -    val eqs = map2 (fn p => fn n => (p,Axiom_eq n)) eq (0 upto (length eq - 1))
     6.8 -    val les = map2 (fn p => fn n => (p,Axiom_le n)) le (0 upto (length le - 1))
     6.9 -    val lts = map2 (fn p => fn n => (p,Axiom_lt n)) lt (0 upto (length lt - 1))
    6.10 +    val eqs = map_index (fn (n, p) => (p,Axiom_eq n)) eq
    6.11 +    val les = map_index (fn (n, p) => (p,Axiom_le n)) le
    6.12 +    val lts = map_index (fn (n, p) => (p,Axiom_lt n)) lt
    6.13     in linear_eqs(eqs,les,lts)
    6.14     end 
    6.15    
     7.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 22 10:52:07 2009 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 22 13:48:06 2009 +0200
     7.3 @@ -102,7 +102,7 @@
     7.4  (**** make datatype info ****)
     7.5  
     7.6  fun make_dt_info descr sorts induct reccomb_names rec_thms
     7.7 -    (((i, (_, (tname, _, _))), distinct), inject) =
     7.8 +    (i, (((_, (tname, _, _)), distinct), inject)) =
     7.9    (tname,
    7.10     {index = i,
    7.11      descr = descr,
    7.12 @@ -2045,8 +2045,8 @@
    7.13        end) (rec_eq_prems ~~
    7.14          DatatypeProp.make_primrecs new_type_names descr' sorts thy12);
    7.15  
    7.16 -    val dt_infos = map (make_dt_info pdescr sorts induct reccomb_names rec_thms)
    7.17 -      ((0 upto length descr1 - 1) ~~ descr1 ~~ distinct_thms ~~ inject_thms);
    7.18 +    val dt_infos = map_index (make_dt_info pdescr sorts induct reccomb_names rec_thms)
    7.19 +      (descr1 ~~ distinct_thms ~~ inject_thms);
    7.20  
    7.21      (* FIXME: theorems are stored in database for testing only *)
    7.22      val (_, thy13) = thy12 |>
     8.1 --- a/src/HOL/SizeChange/sct.ML	Thu Oct 22 10:52:07 2009 +0200
     8.2 +++ b/src/HOL/SizeChange/sct.ML	Thu Oct 22 13:48:06 2009 +0200
     8.3 @@ -156,9 +156,9 @@
     8.4  val mk_number = HOLogic.mk_nat
     8.5  val dest_number = HOLogic.dest_nat
     8.6  
     8.7 -fun nums_to i = map mk_number (0 upto (i - 1))
     8.8 +fun nums_to i = map_range mk_number i
     8.9  
    8.10 -val nth_simps = [thm "List.nth_Cons_0", thm "List.nth_Cons_Suc"]
    8.11 +val nth_simps = [@{thm List.nth_Cons_0}, @{thm List.nth_Cons_Suc}]
    8.12  val nth_ss = (HOL_basic_ss addsimps nth_simps)
    8.13  val simp_nth_tac = simp_tac nth_ss
    8.14  
    8.15 @@ -166,7 +166,7 @@
    8.16  fun tabulate_tlist thy l =
    8.17      let
    8.18        val n = length (HOLogic.dest_list l)
    8.19 -      val table = Inttab.make (map (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) (0 upto n - 1))
    8.20 +      val table = Inttab.make (map_range (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) n)
    8.21      in
    8.22        the o Inttab.lookup table
    8.23      end
    8.24 @@ -250,7 +250,7 @@
    8.25  
    8.26            val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2)
    8.27  
    8.28 -          val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1)))
    8.29 +          val tac = (EVERY (map_range (fn n => EVERY (map_range (set_m1 n) M)) N))
    8.30                        THEN (rtac approx_empty 1)
    8.31  
    8.32            val approx_thm = goal
     9.1 --- a/src/HOL/String.thy	Thu Oct 22 10:52:07 2009 +0200
     9.2 +++ b/src/HOL/String.thy	Thu Oct 22 13:48:06 2009 +0200
     9.3 @@ -48,7 +48,7 @@
     9.4  
     9.5  setup {*
     9.6  let
     9.7 -  val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
     9.8 +  val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
     9.9    val thms = map_product
    9.10     (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
    9.11        nibbles nibbles;
    10.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 22 10:52:07 2009 +0200
    10.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 22 13:48:06 2009 +0200
    10.3 @@ -56,7 +56,7 @@
    10.4      val {maxidx, ...} = rep_thm induct;
    10.5      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    10.6  
    10.7 -    fun prove_casedist_thm ((i, t), T) =
    10.8 +    fun prove_casedist_thm (i, (T, t)) =
    10.9        let
   10.10          val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
   10.11            Abs ("z", T', Const ("True", T''))) induct_Ps;
   10.12 @@ -77,8 +77,8 @@
   10.13               REPEAT (rtac TrueI 1)])
   10.14        end;
   10.15  
   10.16 -    val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
   10.17 -      (DatatypeProp.make_casedists descr sorts) ~~ newTs)
   10.18 +    val casedist_thms = map_index prove_casedist_thm
   10.19 +      (newTs ~~ DatatypeProp.make_casedists descr sorts)
   10.20    in
   10.21      thy
   10.22      |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms
    11.1 --- a/src/HOL/Tools/Function/induction_scheme.ML	Thu Oct 22 10:52:07 2009 +0200
    11.2 +++ b/src/HOL/Tools/Function/induction_scheme.ML	Thu Oct 22 13:48:06 2009 +0200
    11.3 @@ -363,7 +363,7 @@
    11.4  
    11.5      val ineqss = mk_ineqs R scheme
    11.6                     |> map (map (pairself (assume o cert)))
    11.7 -    val complete = map (mk_completeness ctxt scheme #> cert #> assume) (0 upto (length branches - 1))
    11.8 +    val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
    11.9      val wf_thm = mk_wf ctxt R scheme |> cert |> assume
   11.10  
   11.11      val (descent, pres) = split_list (flat ineqss)
    12.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Oct 22 10:52:07 2009 +0200
    12.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Oct 22 13:48:06 2009 +0200
    12.3 @@ -119,7 +119,7 @@
    12.4          G (p, q, edges)
    12.5        end
    12.6    in
    12.7 -    GP (map arity (0 upto n - 1), map mk_graph cs)
    12.8 +    GP (map_range arity n, map mk_graph cs)
    12.9    end
   12.10  
   12.11  (* General reduction pair application *)
   12.12 @@ -312,8 +312,8 @@
   12.13  fun print_error ctxt D = CALLS (fn (cs, i) =>
   12.14    let
   12.15      val np = get_num_points D
   12.16 -    val ms = map (get_measures D) (0 upto np - 1)
   12.17 -    val tys = map (get_types D) (0 upto np - 1)
   12.18 +    val ms = map_range (get_measures D) np
   12.19 +    val tys = map_range (get_types D) np
   12.20      fun index xs = (1 upto length xs) ~~ xs
   12.21      fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
   12.22      val ims = index (map index ms)
    13.1 --- a/src/HOL/Tools/Function/scnp_solve.ML	Thu Oct 22 10:52:07 2009 +0200
    13.2 +++ b/src/HOL/Tools/Function/scnp_solve.ML	Thu Oct 22 13:48:06 2009 +0200
    13.3 @@ -63,8 +63,8 @@
    13.4                         /  \  f i
    13.5                        0<=i<n
    13.6   *)
    13.7 -fun iforall n f = all (map f (0 upto n - 1))
    13.8 -fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
    13.9 +fun iforall n f = all (map_range f n)
   13.10 +fun iexists n f = PropLogic.exists (map_range f n)
   13.11  fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
   13.12  
   13.13  fun the_one var n x = all (var x :: map (Not o var) (remove (op =) x (0 upto n - 1)))
   13.14 @@ -221,7 +221,7 @@
   13.15        let fun prog_pt_mapping p =
   13.16              map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE)
   13.17                (0 upto (arity gp p) - 1)
   13.18 -      in map prog_pt_mapping (0 upto num_prog_pts gp - 1) end
   13.19 +      in map_range prog_pt_mapping (num_prog_pts gp) end
   13.20  
   13.21      val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1)
   13.22  
    14.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Thu Oct 22 10:52:07 2009 +0200
    14.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Thu Oct 22 13:48:06 2009 +0200
    14.3 @@ -312,7 +312,7 @@
    14.4  (* Overall function.                                                         *)
    14.5  
    14.6  fun grobner pols =
    14.7 -    let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1))
    14.8 +    let val npols = map_index (fn (n, p) => (p, Start n)) pols
    14.9          val phists = filter (fn (p,_) => not (null p)) npols
   14.10          val bas = grobner_interreduce [] (map monic phists)
   14.11          val prs0 = map_product pair bas bas
   14.12 @@ -802,8 +802,8 @@
   14.13    val pols = map (grobify_term vars) tms
   14.14    val pol = grobify_term vars tm
   14.15    val cert = grobner_ideal vars pols pol
   14.16 - in map (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars)
   14.17 -        (0 upto (length pols - 1))
   14.18 + in map_range (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars)
   14.19 +   (length pols)
   14.20   end
   14.21  
   14.22  fun poly_eq_conv t = 
    15.1 --- a/src/HOL/Tools/TFL/tfl.ML	Thu Oct 22 10:52:07 2009 +0200
    15.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu Oct 22 13:48:06 2009 +0200
    15.3 @@ -54,8 +54,6 @@
    15.4  
    15.5  val list_mk_type = U.end_itlist (curry (op -->));
    15.6  
    15.7 -fun enumerate xs = ListPair.zip(xs, 0 upto (length xs - 1));
    15.8 -
    15.9  fun front_last [] = raise TFL_ERR "front_last" "empty list"
   15.10    | front_last [x] = ([],x)
   15.11    | front_last (h::t) =
   15.12 @@ -328,7 +326,7 @@
   15.13       val (fname,ftype) = dest_atom atom
   15.14       val dummy = map (no_repeat_vars thy) pats
   15.15       val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
   15.16 -                              map (fn (t,i) => (t,(i,true))) (enumerate R))
   15.17 +                              map_index (fn (i, t) => (t,(i,true))) R)
   15.18       val names = List.foldr OldTerm.add_term_names [] R
   15.19       val atype = type_of(hd pats)
   15.20       and aname = Name.variant names "a"
    16.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Oct 22 10:52:07 2009 +0200
    16.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Oct 22 13:48:06 2009 +0200
    16.3 @@ -625,7 +625,7 @@
    16.4  fun conv_ntuple fs ts p =
    16.5    let
    16.6      val k = length fs;
    16.7 -    val xs = map (fn i => str ("x" ^ string_of_int i)) (0 upto k);
    16.8 +    val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1);
    16.9      val xs' = map (fn Bound i => nth xs (k - i)) ts;
   16.10      fun conv xs js =
   16.11        if js mem fs then
    17.1 --- a/src/HOL/Tools/record.ML	Thu Oct 22 10:52:07 2009 +0200
    17.2 +++ b/src/HOL/Tools/record.ML	Thu Oct 22 13:48:06 2009 +0200
    17.3 @@ -1894,8 +1894,8 @@
    17.4              more;
    17.5        in
    17.6          if more = HOLogic.unit
    17.7 -        then build (map recT (0 upto parent_len))
    17.8 -        else build (map rec_schemeT (0 upto parent_len))
    17.9 +        then build (map_range recT (parent_len + 1))
   17.10 +        else build (map_range rec_schemeT (parent_len + 1))
   17.11        end;
   17.12  
   17.13      val r_rec0 = mk_rec all_vars_more 0;
    18.1 --- a/src/HOL/Tools/refute.ML	Thu Oct 22 10:52:07 2009 +0200
    18.2 +++ b/src/HOL/Tools/refute.ML	Thu Oct 22 13:48:06 2009 +0200
    18.3 @@ -2618,8 +2618,7 @@
    18.4                            "unexpected size of IDT (wrong type associated?)")
    18.5                        else ()
    18.6                    (* interpretation *)
    18.7 -                  val rec_op = Node (map (compute_array_entry idt_index)
    18.8 -                    (0 upto (idt_size - 1)))
    18.9 +                  val rec_op = Node (map_range (compute_array_entry idt_index) idt_size)
   18.10                  in
   18.11                    SOME (rec_op, model', args')
   18.12                  end
   18.13 @@ -2784,8 +2783,8 @@
   18.14                  (replicate (size_of_nat - element - 1) False))
   18.15            end
   18.16        in
   18.17 -        SOME (Node (map (fn m => Node (map (plus m) (0 upto size_of_nat-1)))
   18.18 -          (0 upto size_of_nat-1)), model, args)
   18.19 +        SOME (Node (map_range (fn m => Node (map_range (plus m) size_of_nat)) size_of_nat),
   18.20 +          model, args)
   18.21        end
   18.22      | _ =>
   18.23        NONE;
   18.24 @@ -2812,8 +2811,8 @@
   18.25                (replicate (size_of_nat - element - 1) False))
   18.26            end
   18.27        in
   18.28 -        SOME (Node (map (fn m => Node (map (minus m) (0 upto size_of_nat-1)))
   18.29 -          (0 upto size_of_nat-1)), model, args)
   18.30 +        SOME (Node (map_range (fn m => Node (map_range (minus m) size_of_nat)) size_of_nat),
   18.31 +          model, args)
   18.32        end
   18.33      | _ =>
   18.34        NONE;
   18.35 @@ -2843,8 +2842,8 @@
   18.36                  (replicate (size_of_nat - element - 1) False))
   18.37            end
   18.38        in
   18.39 -        SOME (Node (map (fn m => Node (map (mult m) (0 upto size_of_nat-1)))
   18.40 -          (0 upto size_of_nat-1)), model, args)
   18.41 +        SOME (Node (map_range (fn m => Node (map_range (mult m) size_of_nat)) size_of_nat),
   18.42 +          model, args)
   18.43        end
   18.44      | _ =>
   18.45        NONE;
    19.1 --- a/src/Provers/order.ML	Thu Oct 22 10:52:07 2009 +0200
    19.2 +++ b/src/Provers/order.ML	Thu Oct 22 13:48:06 2009 +0200
    19.3 @@ -731,9 +731,6 @@
    19.4   in u :: dfs_visit g u end;
    19.5  
    19.6  
    19.7 -fun indexComps components =
    19.8 -    ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components);
    19.9 -
   19.10  fun indexNodes IndexComp =
   19.11      maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp;
   19.12  
   19.13 @@ -1109,7 +1106,7 @@
   19.14  |   mk_sccGraphs components leqG neqG ntc =
   19.15      let
   19.16      (* Liste (Index der Komponente, Komponente *)
   19.17 -    val IndexComp = indexComps components;
   19.18 +    val IndexComp = map_index I components;
   19.19  
   19.20  
   19.21      fun handleContr edge g =
   19.22 @@ -1211,7 +1208,7 @@
   19.23   let
   19.24    val (leqG, neqG, neqE) = mkGraphs asms
   19.25    val components = scc_term leqG
   19.26 -  val ntc = indexNodes (indexComps components)
   19.27 +  val ntc = indexNodes (map_index I components)
   19.28    val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc
   19.29   in
   19.30     let
    20.1 --- a/src/Provers/quasi.ML	Thu Oct 22 10:52:07 2009 +0200
    20.2 +++ b/src/Provers/quasi.ML	Thu Oct 22 13:48:06 2009 +0200
    20.3 @@ -118,8 +118,8 @@
    20.4  (*                                                                          *)
    20.5  (* ************************************************************************ *)
    20.6  
    20.7 -fun mkasm_trans sign (t, n) =
    20.8 -  case Less.decomp_trans sign t of
    20.9 +fun mkasm_trans thy (t, n) =
   20.10 +  case Less.decomp_trans thy t of
   20.11      SOME (x, rel, y) =>
   20.12      (case rel of
   20.13       "<="  =>  [Le (x, y, Asm n)]
   20.14 @@ -137,8 +137,8 @@
   20.15  (*                                                                          *)
   20.16  (* ************************************************************************ *)
   20.17  
   20.18 -fun mkasm_quasi sign (t, n) =
   20.19 -  case Less.decomp_quasi sign t of
   20.20 +fun mkasm_quasi thy (t, n) =
   20.21 +  case Less.decomp_quasi thy t of
   20.22      SOME (x, rel, y) => (case rel of
   20.23        "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE))
   20.24                 else [Less (x, y, Asm n)]
   20.25 @@ -164,8 +164,8 @@
   20.26  (* ************************************************************************ *)
   20.27  
   20.28  
   20.29 -fun mkconcl_trans sign t =
   20.30 -  case Less.decomp_trans sign t of
   20.31 +fun mkconcl_trans thy t =
   20.32 +  case Less.decomp_trans thy t of
   20.33      SOME (x, rel, y) => (case rel of
   20.34       "<="  => (Le (x, y, Asm ~1), Asm 0)
   20.35      | _  => raise Cannot)
   20.36 @@ -181,8 +181,8 @@
   20.37  (*                                                                          *)
   20.38  (* ************************************************************************ *)
   20.39  
   20.40 -fun mkconcl_quasi sign t =
   20.41 -  case Less.decomp_quasi sign t of
   20.42 +fun mkconcl_quasi thy t =
   20.43 +  case Less.decomp_quasi thy t of
   20.44      SOME (x, rel, y) => (case rel of
   20.45        "<"   => ([Less (x, y, Asm ~1)], Asm 0)
   20.46      | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
   20.47 @@ -503,12 +503,12 @@
   20.48  (*                                                                         *)
   20.49  (* *********************************************************************** *)
   20.50  
   20.51 -fun solveLeTrans sign (asms, concl) =
   20.52 +fun solveLeTrans thy (asms, concl) =
   20.53   let
   20.54    val g = mkGraph asms
   20.55   in
   20.56     let
   20.57 -    val (subgoal, prf) = mkconcl_trans sign concl
   20.58 +    val (subgoal, prf) = mkconcl_trans thy concl
   20.59      val (found, path) = findPath (lower subgoal) (upper subgoal) g
   20.60     in
   20.61      if found then [getprf (transPath (tl path, hd path))]
   20.62 @@ -526,12 +526,12 @@
   20.63  (*                                                                         *)
   20.64  (* *********************************************************************** *)
   20.65  
   20.66 -fun solveQuasiOrder sign (asms, concl) =
   20.67 +fun solveQuasiOrder thy (asms, concl) =
   20.68   let
   20.69    val (leG, neqE) = mkQuasiGraph asms
   20.70   in
   20.71     let
   20.72 -   val (subgoals, prf) = mkconcl_quasi sign concl
   20.73 +   val (subgoals, prf) = mkconcl_quasi thy concl
   20.74     fun solve facts less =
   20.75         (case triv_solv less of NONE => findQuasiProof (leG, neqE) less
   20.76         | SOME prf => prf )
   20.77 @@ -555,7 +555,7 @@
   20.78    val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
   20.79    val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   20.80    val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
   20.81 -  val lesss = flat (ListPair.map (mkasm_trans thy) (Hs, 0 upto (length Hs - 1)));
   20.82 +  val lesss = flat (map_index (mkasm_trans thy o swap) Hs);
   20.83    val prfs = solveLeTrans thy (lesss, C);
   20.84  
   20.85    val (subgoal, prf) = mkconcl_trans thy C;
   20.86 @@ -576,7 +576,7 @@
   20.87    val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
   20.88    val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   20.89    val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
   20.90 -  val lesss = flat (ListPair.map (mkasm_quasi thy) (Hs, 0 upto (length Hs - 1)));
   20.91 +  val lesss = flat (map_index (mkasm_quasi thy o swap) Hs);
   20.92    val prfs = solveQuasiOrder thy (lesss, C);
   20.93    val (subgoals, prf) = mkconcl_quasi thy C;
   20.94   in
    21.1 --- a/src/Provers/trancl.ML	Thu Oct 22 10:52:07 2009 +0200
    21.2 +++ b/src/Provers/trancl.ML	Thu Oct 22 13:48:06 2009 +0200
    21.3 @@ -538,7 +538,7 @@
    21.4    val C = Logic.strip_assums_concl A;
    21.5    val (rel, subgoals, prf) = mkconcl_trancl C;
    21.6  
    21.7 -  val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));
    21.8 +  val prems = flat (map_index (mkasm_trancl rel o swap) Hs);
    21.9    val prfs = solveTrancl (prems, C);
   21.10   in
   21.11    Subgoal.FOCUS (fn {prems, ...} =>
   21.12 @@ -555,7 +555,7 @@
   21.13    val C = Logic.strip_assums_concl A;
   21.14    val (rel, subgoals, prf) = mkconcl_rtrancl C;
   21.15  
   21.16 -  val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));
   21.17 +  val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
   21.18    val prfs = solveRtrancl (prems, C);
   21.19   in
   21.20    Subgoal.FOCUS (fn {prems, ...} =>
    22.1 --- a/src/Pure/Syntax/parser.ML	Thu Oct 22 10:52:07 2009 +0200
    22.2 +++ b/src/Pure/Syntax/parser.ML	Thu Oct 22 13:48:06 2009 +0200
    22.3 @@ -840,7 +840,7 @@
    22.4  
    22.5  fun guess_infix_lr (Gram gram) c = (*based on educated guess*)
    22.6    let
    22.7 -    fun freeze a = map (curry Array.sub a) (0 upto Array.length a - 1);
    22.8 +    fun freeze a = map_range (curry Array.sub a) (Array.length a);
    22.9      val prods = maps snd (maps snd (freeze (#prods gram)));
   22.10      fun guess (SOME ([Nonterminal (_, k), Terminal (Token (Literal, s, _)), Nonterminal (_, l)], _, j)) =
   22.11            if k = j andalso l = j + 1 then SOME (s, true, false, j)
    23.1 --- a/src/Pure/library.ML	Thu Oct 22 10:52:07 2009 +0200
    23.2 +++ b/src/Pure/library.ML	Thu Oct 22 13:48:06 2009 +0200
    23.3 @@ -89,6 +89,7 @@
    23.4    val nth_list: 'a list list -> int -> 'a list
    23.5    val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
    23.6    val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    23.7 +  val map_range: (int -> 'a) -> int -> 'a list
    23.8    val split_last: 'a list -> 'a list * 'a
    23.9    val find_index: ('a -> bool) -> 'a list -> int
   23.10    val find_first: ('a -> bool) -> 'a list -> 'a option
   23.11 @@ -463,6 +464,12 @@
   23.12        | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y);
   23.13    in fold_aux 0 end;
   23.14  
   23.15 +fun map_range f i =
   23.16 +  let
   23.17 +    fun mapp k =
   23.18 +      if k < i then f k :: mapp (k + 1) else [];
   23.19 +  in mapp 0 end;
   23.20 +
   23.21  val last_elem = List.last;
   23.22  
   23.23  (*rear decomposition*)
    24.1 --- a/src/Pure/term.ML	Thu Oct 22 10:52:07 2009 +0200
    24.2 +++ b/src/Pure/term.ML	Thu Oct 22 13:48:06 2009 +0200
    24.3 @@ -939,7 +939,7 @@
    24.4    | free_dummy_patterns a used = (a, used);
    24.5  
    24.6  fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
    24.7 -      (list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)), i + 1)
    24.8 +      (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
    24.9    | replace_dummy Ts (Abs (x, T, t)) i =
   24.10        let val (t', i') = replace_dummy (T :: Ts) t i
   24.11        in (Abs (x, T, t'), i') end
    25.1 --- a/src/Pure/unify.ML	Thu Oct 22 10:52:07 2009 +0200
    25.2 +++ b/src/Pure/unify.ML	Thu Oct 22 13:48:06 2009 +0200
    25.3 @@ -531,12 +531,12 @@
    25.4    Bound vars in the binder are "banned" unless used in both t AND u *)
    25.5  fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) =
    25.6    let val loot = loose_bnos t  and  loou = loose_bnos u
    25.7 -      fun add_index (((a,T), j), (bnos, newbinder)) =
    25.8 +      fun add_index (j, (a,T)) (bnos, newbinder) =
    25.9              if  member (op =) loot j  andalso  member (op =) loou j
   25.10              then  (bnos, (a,T)::newbinder)  (*needed by both: keep*)
   25.11              else  (j::bnos, newbinder);   (*remove*)
   25.12 -      val indices = 0 upto (length rbinder - 1);
   25.13 -      val (banned,rbin') = List.foldr add_index ([],[]) (rbinder~~indices);
   25.14 +      val (banned,rbin') = fold_rev add_index
   25.15 +        ((0 upto (length rbinder - 1)) ~~ rbinder) ([],[]);
   25.16        val (env', t') = clean_term banned (env, t);
   25.17        val (env'',u') = clean_term banned (env',u)
   25.18    in  (ff_assign thy (env'', rbin', t', u'), tpairs)
    26.1 --- a/src/Tools/Code/code_preproc.ML	Thu Oct 22 10:52:07 2009 +0200
    26.2 +++ b/src/Tools/Code/code_preproc.ML	Thu Oct 22 13:48:06 2009 +0200
    26.3 @@ -408,9 +408,8 @@
    26.4    in Thm.instantiate (insts, []) thm end;
    26.5  
    26.6  fun add_arity thy vardeps (class, tyco) =
    26.7 -  AList.default (op =)
    26.8 -    ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
    26.9 -      (0 upto Sign.arity_number thy tyco - 1));
   26.10 +  AList.default (op =) ((class, tyco),
   26.11 +    map_range (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) (Sign.arity_number thy tyco));
   26.12  
   26.13  fun add_eqs thy vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
   26.14    if can (Graph.get_node eqngr) c then (rhss, eqngr)