# HG changeset patch # User haftmann # Date 1256213281 -7200 # Node ID ba7ff3f9527a11c435917beba23341b610867961 # Parent d1c9bf0f8ae8e22768dcd7f53b00c960c72d7b4f# Parent 4d462963a7db5d381ed40b9fb6ead49bf53111d5 merged diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/FOLP/simp.ML --- a/src/FOLP/simp.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/FOLP/simp.ML Thu Oct 22 14:08:01 2009 +0200 @@ -534,7 +534,7 @@ fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) = let fun xn_list(x,n) = - let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n); + let val ixs = map_range (fn i => (x^(radixstring(26,"a",i)),0)) (n - 1); in ListPair.map eta_Var (ixs, Library.take(n+1,Ts)) end val lhs = list_comb(f,xn_list("X",k-1)) val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik) diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Thu Oct 22 14:08:01 2009 +0200 @@ -2035,8 +2035,8 @@ val t = Thm.term_of ct; val fs = OldTerm.term_frees t; val bs = term_bools [] t; - val vs = fs ~~ (0 upto (length fs - 1)) - val ps = bs ~~ (0 upto (length bs - 1)) + val vs = map_index swap fs; + val ps = map_index swap bs; val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t; in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end end; diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Oct 22 14:08:01 2009 +0200 @@ -2073,7 +2073,7 @@ val thy = Thm.theory_of_cterm ct; val t = Thm.term_of ct; val fs = OldTerm.term_frees t; - val vs = fs ~~ (0 upto (length fs - 1)); + val vs = map_index swap fs; val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t)))); in Thm.cterm_of thy res end end; diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Oct 22 14:08:01 2009 +0200 @@ -5898,7 +5898,7 @@ val thy = Thm.theory_of_cterm ct; val t = Thm.term_of ct; val fs = OldTerm.term_frees t; - val vs = fs ~~ (0 upto (length fs - 1)); + val vs = map_index swap fs; val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe}; val t' = (term_of_fm vs o qe o fm_of_term vs) t; in (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu Oct 22 14:08:01 2009 +0200 @@ -965,8 +965,8 @@ else if d = 0 then [FuncUtil.Ctermfunc.empty] else if null vars then [monomial_1] else let val alts = - map (fn k => let val oths = enumerate_monomials (d - k) (tl vars) - in map (fn ks => if k = 0 then ks else FuncUtil.Ctermfunc.update (hd vars, k) ks) oths end) (0 upto d) + map_range (fn k => let val oths = enumerate_monomials (d - k) (tl vars) + in map (fn ks => if k = 0 then ks else FuncUtil.Ctermfunc.update (hd vars, k) ks) oths end) (d + 1) in flat alts end; @@ -1202,9 +1202,9 @@ val eq0 = map (poly_of_term o Thm.dest_arg1 o concl) eqs val le0 = map (poly_of_term o Thm.dest_arg o concl) les val lt0 = map (poly_of_term o Thm.dest_arg o concl) lts - val eqp0 = map (fn (t,i) => (t,RealArith.Axiom_eq i)) (eq0 ~~ (0 upto (length eq0 - 1))) - val lep0 = map (fn (t,i) => (t,RealArith.Axiom_le i)) (le0 ~~ (0 upto (length le0 - 1))) - val ltp0 = map (fn (t,i) => (t,RealArith.Axiom_lt i)) (lt0 ~~ (0 upto (length lt0 - 1))) + val eqp0 = map_index (fn (i, t) => (t,RealArith.Axiom_eq i)) eq0 + val lep0 = map_index (fn (i, t) => (t,RealArith.Axiom_le i)) le0 + val ltp0 = map_index (fn (i, t) => (t,RealArith.Axiom_lt i)) lt0 val (keq,eq) = List.partition (fn (p,_) => multidegree p = 0) eqp0 val (klep,lep) = List.partition (fn (p,_) => multidegree p = 0) lep0 val (kltp,ltp) = List.partition (fn (p,_) => multidegree p = 0) ltp0 diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Thu Oct 22 14:08:01 2009 +0200 @@ -643,9 +643,9 @@ fun linear_prover (eq,le,lt) = let - val eqs = map2 (fn p => fn n => (p,Axiom_eq n)) eq (0 upto (length eq - 1)) - val les = map2 (fn p => fn n => (p,Axiom_le n)) le (0 upto (length le - 1)) - val lts = map2 (fn p => fn n => (p,Axiom_lt n)) lt (0 upto (length lt - 1)) + val eqs = map_index (fn (n, p) => (p,Axiom_eq n)) eq + val les = map_index (fn (n, p) => (p,Axiom_le n)) le + val lts = map_index (fn (n, p) => (p,Axiom_lt n)) lt in linear_eqs(eqs,les,lts) end diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Thu Oct 22 14:08:01 2009 +0200 @@ -102,7 +102,7 @@ (**** make datatype info ****) fun make_dt_info descr sorts induct reccomb_names rec_thms - (((i, (_, (tname, _, _))), distinct), inject) = + (i, (((_, (tname, _, _)), distinct), inject)) = (tname, {index = i, descr = descr, @@ -2045,8 +2045,8 @@ end) (rec_eq_prems ~~ DatatypeProp.make_primrecs new_type_names descr' sorts thy12); - val dt_infos = map (make_dt_info pdescr sorts induct reccomb_names rec_thms) - ((0 upto length descr1 - 1) ~~ descr1 ~~ distinct_thms ~~ inject_thms); + val dt_infos = map_index (make_dt_info pdescr sorts induct reccomb_names rec_thms) + (descr1 ~~ distinct_thms ~~ inject_thms); (* FIXME: theorems are stored in database for testing only *) val (_, thy13) = thy12 |> diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/SizeChange/sct.ML --- a/src/HOL/SizeChange/sct.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/SizeChange/sct.ML Thu Oct 22 14:08:01 2009 +0200 @@ -156,9 +156,9 @@ val mk_number = HOLogic.mk_nat val dest_number = HOLogic.dest_nat -fun nums_to i = map mk_number (0 upto (i - 1)) +fun nums_to i = map_range mk_number i -val nth_simps = [thm "List.nth_Cons_0", thm "List.nth_Cons_Suc"] +val nth_simps = [@{thm List.nth_Cons_0}, @{thm List.nth_Cons_Suc}] val nth_ss = (HOL_basic_ss addsimps nth_simps) val simp_nth_tac = simp_tac nth_ss @@ -166,7 +166,7 @@ fun tabulate_tlist thy l = let val n = length (HOLogic.dest_list l) - 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)) + val table = Inttab.make (map_range (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) n) in the o Inttab.lookup table end @@ -250,7 +250,7 @@ val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2) - val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1))) + val tac = (EVERY (map_range (fn n => EVERY (map_range (set_m1 n) M)) N)) THEN (rtac approx_empty 1) val approx_thm = goal diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/String.thy --- a/src/HOL/String.thy Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/String.thy Thu Oct 22 14:08:01 2009 +0200 @@ -48,7 +48,7 @@ setup {* let - val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15); + val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16; val thms = map_product (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps}) nibbles nibbles; diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Thu Oct 22 14:08:01 2009 +0200 @@ -26,7 +26,6 @@ val info_of_constr : theory -> string * typ -> info option val info_of_case : theory -> string -> info option val interpretation : (config -> string list -> theory -> theory) -> theory -> theory - val distinct_simproc : simproc val make_case : Proof.context -> DatatypeCase.config -> string list -> term -> (term * term) list -> term * (term * (int * bool)) list val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option @@ -159,49 +158,6 @@ (** various auxiliary **) -(* simplification procedure for showing distinctness of constructors *) - -fun stripT (i, Type ("fun", [_, T])) = stripT (i + 1, T) - | stripT p = p; - -fun stripC (i, f $ x) = stripC (i + 1, f) - | stripC p = p; - -val distinctN = "constr_distinct"; - -fun distinct_rule thy ss tname eq_t = Goal.prove (Simplifier.the_context ss) [] [] eq_t - (K (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1, - atac 2, resolve_tac (#distinct (the_info thy tname)) 1, etac FalseE 1])); - -fun get_constr thy dtco = - get_info thy dtco - |> Option.map (fn { descr, index, ... } => (#3 o the o AList.lookup (op =) descr) index); - -fun distinct_proc thy ss (t as Const ("op =", _) $ t1 $ t2) = - (case (stripC (0, t1), stripC (0, t2)) of - ((i, Const (cname1, T1)), (j, Const (cname2, T2))) => - (case (stripT (0, T1), stripT (0, T2)) of - ((i', Type (tname1, _)), (j', Type (tname2, _))) => - if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then - (case get_constr thy tname1 of - SOME constrs => let val cnames = map fst constrs - in if cname1 mem cnames andalso cname2 mem cnames then - SOME (distinct_rule thy ss tname1 - (Logic.mk_equals (t, HOLogic.false_const))) - else NONE - end - | NONE => NONE) - else NONE - | _ => NONE) - | _ => NONE) - | distinct_proc _ _ _ = NONE; - -val distinct_simproc = - Simplifier.simproc @{theory HOL} distinctN ["s = t"] distinct_proc; - -val simproc_setup = - Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]); - (* prepare datatype specifications *) fun read_typ thy ((Ts, sorts), str) = @@ -271,7 +227,8 @@ [("_case_syntax", DatatypeCase.case_tr true info_of_constr)], [], []); -(* document antiquotation *) + +(** document antiquotation **) val _ = ThyOutput.antiquotation "datatype" Args.tyname (fn {source = src, context = ctxt, ...} => fn dtco => @@ -593,4 +550,3 @@ end; end; - diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 22 14:08:01 2009 +0200 @@ -56,7 +56,7 @@ val {maxidx, ...} = rep_thm induct; val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct))); - fun prove_casedist_thm ((i, t), T) = + fun prove_casedist_thm (i, (T, t)) = let val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) => Abs ("z", T', Const ("True", T''))) induct_Ps; @@ -77,8 +77,8 @@ REPEAT (rtac TrueI 1)]) end; - val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~ - (DatatypeProp.make_casedists descr sorts) ~~ newTs) + val casedist_thms = map_index prove_casedist_thm + (newTs ~~ DatatypeProp.make_casedists descr sorts) in thy |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Tools/Function/induction_scheme.ML --- a/src/HOL/Tools/Function/induction_scheme.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Tools/Function/induction_scheme.ML Thu Oct 22 14:08:01 2009 +0200 @@ -363,7 +363,7 @@ val ineqss = mk_ineqs R scheme |> map (map (pairself (assume o cert))) - val complete = map (mk_completeness ctxt scheme #> cert #> assume) (0 upto (length branches - 1)) + val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches) val wf_thm = mk_wf ctxt R scheme |> cert |> assume val (descent, pres) = split_list (flat ineqss) diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Tools/Function/scnp_reconstruct.ML --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Oct 22 14:08:01 2009 +0200 @@ -119,7 +119,7 @@ G (p, q, edges) end in - GP (map arity (0 upto n - 1), map mk_graph cs) + GP (map_range arity n, map mk_graph cs) end (* General reduction pair application *) @@ -312,8 +312,8 @@ fun print_error ctxt D = CALLS (fn (cs, i) => let val np = get_num_points D - val ms = map (get_measures D) (0 upto np - 1) - val tys = map (get_types D) (0 upto np - 1) + val ms = map_range (get_measures D) np + val tys = map_range (get_types D) np fun index xs = (1 upto length xs) ~~ xs fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs val ims = index (map index ms) diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Tools/Function/scnp_solve.ML --- a/src/HOL/Tools/Function/scnp_solve.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Tools/Function/scnp_solve.ML Thu Oct 22 14:08:01 2009 +0200 @@ -63,8 +63,8 @@ / \ f i 0<=i if assign (P(p, x)) then SOME (x, assignTag p x) else NONE) (0 upto (arity gp p) - 1) - in map prog_pt_mapping (0 upto num_prog_pts gp - 1) end + in map_range prog_pt_mapping (num_prog_pts gp) end val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1) diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Thu Oct 22 14:08:01 2009 +0200 @@ -312,7 +312,7 @@ (* Overall function. *) fun grobner pols = - let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1)) + let val npols = map_index (fn (n, p) => (p, Start n)) pols val phists = filter (fn (p,_) => not (null p)) npols val bas = grobner_interreduce [] (map monic phists) val prs0 = map_product pair bas bas @@ -802,8 +802,8 @@ val pols = map (grobify_term vars) tms val pol = grobify_term vars tm val cert = grobner_ideal vars pols pol - in map (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars) - (0 upto (length pols - 1)) + in map_range (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars) + (length pols) end fun poly_eq_conv t = diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Thu Oct 22 14:08:01 2009 +0200 @@ -54,8 +54,6 @@ val list_mk_type = U.end_itlist (curry (op -->)); -fun enumerate xs = ListPair.zip(xs, 0 upto (length xs - 1)); - fun front_last [] = raise TFL_ERR "front_last" "empty list" | front_last [x] = ([],x) | front_last (h::t) = @@ -328,7 +326,7 @@ val (fname,ftype) = dest_atom atom val dummy = map (no_repeat_vars thy) pats val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats, - map (fn (t,i) => (t,(i,true))) (enumerate R)) + map_index (fn (i, t) => (t,(i,true))) R) val names = List.foldr OldTerm.add_term_names [] R val atype = type_of(hd pats) and aname = Name.variant names "a" diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Thu Oct 22 14:08:01 2009 +0200 @@ -625,7 +625,7 @@ fun conv_ntuple fs ts p = let val k = length fs; - val xs = map (fn i => str ("x" ^ string_of_int i)) (0 upto k); + val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1); val xs' = map (fn Bound i => nth xs (k - i)) ts; fun conv xs js = if js mem fs then diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Tools/record.ML Thu Oct 22 14:08:01 2009 +0200 @@ -1894,8 +1894,8 @@ more; in if more = HOLogic.unit - then build (map recT (0 upto parent_len)) - else build (map rec_schemeT (0 upto parent_len)) + then build (map_range recT (parent_len + 1)) + else build (map_range rec_schemeT (parent_len + 1)) end; val r_rec0 = mk_rec all_vars_more 0; diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/HOL/Tools/refute.ML Thu Oct 22 14:08:01 2009 +0200 @@ -2618,8 +2618,7 @@ "unexpected size of IDT (wrong type associated?)") else () (* interpretation *) - val rec_op = Node (map (compute_array_entry idt_index) - (0 upto (idt_size - 1))) + val rec_op = Node (map_range (compute_array_entry idt_index) idt_size) in SOME (rec_op, model', args') end @@ -2784,8 +2783,8 @@ (replicate (size_of_nat - element - 1) False)) end in - SOME (Node (map (fn m => Node (map (plus m) (0 upto size_of_nat-1))) - (0 upto size_of_nat-1)), model, args) + SOME (Node (map_range (fn m => Node (map_range (plus m) size_of_nat)) size_of_nat), + model, args) end | _ => NONE; @@ -2812,8 +2811,8 @@ (replicate (size_of_nat - element - 1) False)) end in - SOME (Node (map (fn m => Node (map (minus m) (0 upto size_of_nat-1))) - (0 upto size_of_nat-1)), model, args) + SOME (Node (map_range (fn m => Node (map_range (minus m) size_of_nat)) size_of_nat), + model, args) end | _ => NONE; @@ -2843,8 +2842,8 @@ (replicate (size_of_nat - element - 1) False)) end in - SOME (Node (map (fn m => Node (map (mult m) (0 upto size_of_nat-1))) - (0 upto size_of_nat-1)), model, args) + SOME (Node (map_range (fn m => Node (map_range (mult m) size_of_nat)) size_of_nat), + model, args) end | _ => NONE; diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/Provers/order.ML --- a/src/Provers/order.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/Provers/order.ML Thu Oct 22 14:08:01 2009 +0200 @@ -731,9 +731,6 @@ in u :: dfs_visit g u end; -fun indexComps components = - ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components); - fun indexNodes IndexComp = maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp; @@ -1109,7 +1106,7 @@ | mk_sccGraphs components leqG neqG ntc = let (* Liste (Index der Komponente, Komponente *) - val IndexComp = indexComps components; + val IndexComp = map_index I components; fun handleContr edge g = @@ -1211,7 +1208,7 @@ let val (leqG, neqG, neqE) = mkGraphs asms val components = scc_term leqG - val ntc = indexNodes (indexComps components) + val ntc = indexNodes (map_index I components) val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc in let diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/Provers/quasi.ML --- a/src/Provers/quasi.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/Provers/quasi.ML Thu Oct 22 14:08:01 2009 +0200 @@ -118,8 +118,8 @@ (* *) (* ************************************************************************ *) -fun mkasm_trans sign (t, n) = - case Less.decomp_trans sign t of +fun mkasm_trans thy (t, n) = + case Less.decomp_trans thy t of SOME (x, rel, y) => (case rel of "<=" => [Le (x, y, Asm n)] @@ -137,8 +137,8 @@ (* *) (* ************************************************************************ *) -fun mkasm_quasi sign (t, n) = - case Less.decomp_quasi sign t of +fun mkasm_quasi thy (t, n) = + case Less.decomp_quasi thy t of SOME (x, rel, y) => (case rel of "<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) else [Less (x, y, Asm n)] @@ -164,8 +164,8 @@ (* ************************************************************************ *) -fun mkconcl_trans sign t = - case Less.decomp_trans sign t of +fun mkconcl_trans thy t = + case Less.decomp_trans thy t of SOME (x, rel, y) => (case rel of "<=" => (Le (x, y, Asm ~1), Asm 0) | _ => raise Cannot) @@ -181,8 +181,8 @@ (* *) (* ************************************************************************ *) -fun mkconcl_quasi sign t = - case Less.decomp_quasi sign t of +fun mkconcl_quasi thy t = + case Less.decomp_quasi thy t of SOME (x, rel, y) => (case rel of "<" => ([Less (x, y, Asm ~1)], Asm 0) | "<=" => ([Le (x, y, Asm ~1)], Asm 0) @@ -503,12 +503,12 @@ (* *) (* *********************************************************************** *) -fun solveLeTrans sign (asms, concl) = +fun solveLeTrans thy (asms, concl) = let val g = mkGraph asms in let - val (subgoal, prf) = mkconcl_trans sign concl + val (subgoal, prf) = mkconcl_trans thy concl val (found, path) = findPath (lower subgoal) (upper subgoal) g in if found then [getprf (transPath (tl path, hd path))] @@ -526,12 +526,12 @@ (* *) (* *********************************************************************** *) -fun solveQuasiOrder sign (asms, concl) = +fun solveQuasiOrder thy (asms, concl) = let val (leG, neqE) = mkQuasiGraph asms in let - val (subgoals, prf) = mkconcl_quasi sign concl + val (subgoals, prf) = mkconcl_quasi thy concl fun solve facts less = (case triv_solv less of NONE => findQuasiProof (leG, neqE) less | SOME prf => prf ) @@ -555,7 +555,7 @@ val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); val C = subst_bounds (rfrees, Logic.strip_assums_concl A); - val lesss = flat (ListPair.map (mkasm_trans thy) (Hs, 0 upto (length Hs - 1))); + val lesss = flat (map_index (mkasm_trans thy o swap) Hs); val prfs = solveLeTrans thy (lesss, C); val (subgoal, prf) = mkconcl_trans thy C; @@ -576,7 +576,7 @@ val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); val C = subst_bounds (rfrees, Logic.strip_assums_concl A); - val lesss = flat (ListPair.map (mkasm_quasi thy) (Hs, 0 upto (length Hs - 1))); + val lesss = flat (map_index (mkasm_quasi thy o swap) Hs); val prfs = solveQuasiOrder thy (lesss, C); val (subgoals, prf) = mkconcl_quasi thy C; in diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/Provers/trancl.ML --- a/src/Provers/trancl.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/Provers/trancl.ML Thu Oct 22 14:08:01 2009 +0200 @@ -538,7 +538,7 @@ val C = Logic.strip_assums_concl A; val (rel, subgoals, prf) = mkconcl_trancl C; - val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1))); + val prems = flat (map_index (mkasm_trancl rel o swap) Hs); val prfs = solveTrancl (prems, C); in Subgoal.FOCUS (fn {prems, ...} => @@ -555,7 +555,7 @@ val C = Logic.strip_assums_concl A; val (rel, subgoals, prf) = mkconcl_rtrancl C; - val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1))); + val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs); val prfs = solveRtrancl (prems, C); in Subgoal.FOCUS (fn {prems, ...} => diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/Pure/Syntax/parser.ML Thu Oct 22 14:08:01 2009 +0200 @@ -840,7 +840,7 @@ fun guess_infix_lr (Gram gram) c = (*based on educated guess*) let - fun freeze a = map (curry Array.sub a) (0 upto Array.length a - 1); + fun freeze a = map_range (curry Array.sub a) (Array.length a); val prods = maps snd (maps snd (freeze (#prods gram))); fun guess (SOME ([Nonterminal (_, k), Terminal (Token (Literal, s, _)), Nonterminal (_, l)], _, j)) = if k = j andalso l = j + 1 then SOME (s, true, false, j) diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/Pure/library.ML --- a/src/Pure/library.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/Pure/library.ML Thu Oct 22 14:08:01 2009 +0200 @@ -89,6 +89,7 @@ val nth_list: 'a list list -> int -> 'a list val map_index: (int * 'a -> 'b) -> 'a list -> 'b list val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b + val map_range: (int -> 'a) -> int -> 'a list val split_last: 'a list -> 'a list * 'a val find_index: ('a -> bool) -> 'a list -> int val find_first: ('a -> bool) -> 'a list -> 'a option @@ -463,6 +464,12 @@ | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y); in fold_aux 0 end; +fun map_range f i = + let + fun mapp k = + if k < i then f k :: mapp (k + 1) else []; + in mapp 0 end; + val last_elem = List.last; (*rear decomposition*) diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/Pure/term.ML --- a/src/Pure/term.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/Pure/term.ML Thu Oct 22 14:08:01 2009 +0200 @@ -939,7 +939,7 @@ | free_dummy_patterns a used = (a, used); fun replace_dummy Ts (Const ("dummy_pattern", T)) i = - (list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)), i + 1) + (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1) | replace_dummy Ts (Abs (x, T, t)) i = let val (t', i') = replace_dummy (T :: Ts) t i in (Abs (x, T, t'), i') end diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/Pure/unify.ML --- a/src/Pure/unify.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/Pure/unify.ML Thu Oct 22 14:08:01 2009 +0200 @@ -531,12 +531,12 @@ Bound vars in the binder are "banned" unless used in both t AND u *) fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) = let val loot = loose_bnos t and loou = loose_bnos u - fun add_index (((a,T), j), (bnos, newbinder)) = + fun add_index (j, (a,T)) (bnos, newbinder) = if member (op =) loot j andalso member (op =) loou j then (bnos, (a,T)::newbinder) (*needed by both: keep*) else (j::bnos, newbinder); (*remove*) - val indices = 0 upto (length rbinder - 1); - val (banned,rbin') = List.foldr add_index ([],[]) (rbinder~~indices); + val (banned,rbin') = fold_rev add_index + ((0 upto (length rbinder - 1)) ~~ rbinder) ([],[]); val (env', t') = clean_term banned (env, t); val (env'',u') = clean_term banned (env',u) in (ff_assign thy (env'', rbin', t', u'), tpairs) diff -r d1c9bf0f8ae8 -r ba7ff3f9527a src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Thu Oct 22 09:50:29 2009 +0200 +++ b/src/Tools/Code/code_preproc.ML Thu Oct 22 14:08:01 2009 +0200 @@ -408,9 +408,8 @@ in Thm.instantiate (insts, []) thm end; fun add_arity thy vardeps (class, tyco) = - AList.default (op =) - ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) - (0 upto Sign.arity_number thy tyco - 1)); + AList.default (op =) ((class, tyco), + map_range (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) (Sign.arity_number thy tyco)); fun add_eqs thy vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) = if can (Graph.get_node eqngr) c then (rhss, eqngr)