--- a/src/HOL/Nominal/nominal_atoms.ML Wed Dec 05 14:15:59 2007 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Dec 05 14:16:05 2007 +0100
@@ -817,20 +817,20 @@
in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end;
(* list of all dj_inst-theorems *)
val djs =
- let fun djs_fun (ak1,ak2) =
+ let fun djs_fun ak1 ak2 =
if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 (Name ("dj_"^ak2^"_"^ak1)))
- in List.mapPartial I (map djs_fun (Library.product ak_names ak_names)) end;
+ in map_filter I (map_product djs_fun ak_names ak_names) end;
(* list of all fs_inst-theorems *)
val fss = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"_inst"))) ak_names
(* list of all at_inst-theorems *)
val fs_axs = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"1"))) ak_names
- fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms);
- fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms);
- fun inst_fs thms = Library.flat (map (fn ti => instR ti fss) thms);
- fun inst_cp thms cps = Library.flat (inst_mult thms cps);
+ fun inst_pt thms = maps (fn ti => instR ti pts) thms;
+ fun inst_at thms = maps (fn ti => instR ti ats) thms;
+ fun inst_fs thms = maps (fn ti => instR ti fss) thms;
+ fun inst_cp thms cps = flat (inst_mult thms cps);
fun inst_pt_at thms = inst_zip ats (inst_pt thms);
- fun inst_dj thms = Library.flat (map (fn ti => instR ti djs) thms);
+ fun inst_dj thms = maps (fn ti => instR ti djs) thms;
fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps;
fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms));
fun inst_pt_pt_at_cp thms =
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Dec 05 14:15:59 2007 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Dec 05 14:16:05 2007 +0100
@@ -316,7 +316,7 @@
let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1))
val phists = filter (fn (p,_) => not (null p)) npols
val bas = grobner_interreduce [] (map monic phists)
- val prs0 = product bas bas
+ val prs0 = map_product pair bas bas
val prs1 = filter (fn ((x,_),(y,_)) => poly_lt x y) prs0
val prs2 = map (fn (p,q) => (mlcm (hd(fst p)) (hd(fst q)),(p,q))) prs1
val prs3 =
--- a/src/HOL/Tools/function_package/context_tree.ML Wed Dec 05 14:15:59 2007 +0100
+++ b/src/HOL/Tools/function_package/context_tree.ML Wed Dec 05 14:16:05 2007 +0100
@@ -97,8 +97,8 @@
in
IntGraph.empty
|> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
- |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
- (product num_branches num_branches)
+ |> fold_product (fn (i,(c1,_)) => fn (j,(_, t2)) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
+ num_branches num_branches
end
val add_congs = map (fn c => c RS eq_reflection) [cong, ext]
--- a/src/HOL/Tools/function_package/lexicographic_order.ML Wed Dec 05 14:15:59 2007 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Wed Dec 05 14:16:05 2007 +0100
@@ -120,8 +120,7 @@
| mk_funorder_funs T = [ constant_1 T ]
fun mk_ext_base_funs thy (Type("+", [fT, sT])) =
- product (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT)
- |> map (uncurry mk_sum_case)
+ map_product mk_sum_case (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT)
| mk_ext_base_funs thy T = mk_base_funs thy T
fun mk_all_measure_funs thy (T as Type ("+", _)) =
--- a/src/HOL/Tools/function_package/pattern_split.ML Wed Dec 05 14:15:59 2007 +0100
+++ b/src/HOL/Tools/function_package/pattern_split.ML Wed Dec 05 14:16:05 2007 +0100
@@ -48,7 +48,7 @@
fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
-fun join_product (xs, ys) = map join (product xs ys)
+fun join_product (xs, ys) = map_product (curry join) xs ys
fun join_list [] = []
| join_list xs = foldr1 (join_product) xs
--- a/src/HOL/Tools/refute.ML Wed Dec 05 14:15:59 2007 +0100
+++ b/src/HOL/Tools/refute.ML Wed Dec 05 14:16:05 2007 +0100
@@ -2181,7 +2181,7 @@
(* C_i x_1 ... x_n < C_i y_1 ... y_n if *)
(* (x_1, ..., x_n) < (y_1, ..., y_n) *)
constructor_terms
- (map (op $) (Library.product terms d_terms)) ds
+ (map_product (curry op $) terms d_terms) ds
end
in
(* C_i ... < C_j ... if i < j *)
--- a/src/Pure/General/graph.ML Wed Dec 05 14:15:59 2007 +0100
+++ b/src/Pure/General/graph.ML Wed Dec 05 14:16:05 2007 +0100
@@ -257,7 +257,7 @@
fun add_edge_trans_acyclic (x, y) G =
add_edge_acyclic (x, y) G
- |> fold add_edge (Library.product (all_preds G [x]) (all_succs G [y]));
+ |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]);
fun merge_trans_acyclic eq (G1, G2) =
merge_acyclic eq (G1, G2)
--- a/src/Pure/library.ML Wed Dec 05 14:15:59 2007 +0100
+++ b/src/Pure/library.ML Wed Dec 05 14:16:05 2007 +0100
@@ -100,13 +100,14 @@
val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+ val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+ val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
val zip_options: 'a list -> 'b option list -> ('a * 'b) list
val ~~ : 'a list * 'b list -> ('a * 'b) list
val split_list: ('a * 'b) list -> 'a list * 'b list
val separate: 'a -> 'a list -> 'a list
val replicate: int -> 'a -> 'a list
val multiply: 'a list -> 'a list list -> 'a list list
- val product: 'a list -> 'b list -> ('a * 'b) list
val filter: ('a -> bool) -> 'a list -> 'a list
val filter_out: ('a -> bool) -> 'a list -> 'a list
val map_filter: ('a -> 'b option) -> 'a list -> 'b list
@@ -429,6 +430,11 @@
fun maps f [] = []
| maps f (x :: xs) = f x @ maps f xs;
+(*copy the list preserving elements that satisfy the predicate*)
+val filter = List.filter;
+fun filter_out f = filter (not o f);
+val map_filter = List.mapPartial;
+
fun chop (0: int) xs = ([], xs)
| chop _ [] = ([], [])
| chop n (x :: xs) = chop (n - 1) xs |>> cons x;
@@ -540,20 +546,15 @@
| multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
(*direct product*)
-fun product _ [] = []
- | product [] _ = []
- | product (x :: xs) ys = map (pair x) ys @ product xs ys;
-
-
-(* filter *)
+fun map_product f _ [] = []
+ | map_product f [] _ = []
+ | map_product f (x :: xs) ys = map (f x) ys @ map_product f xs ys;
-(*copy the list preserving elements that satisfy the predicate*)
-val filter = List.filter;
-fun filter_out f = filter (not o f);
-val map_filter = List.mapPartial;
+fun fold_product f _ [] z = z
+ | fold_product f [] _ z = z
+ | fold_product f (x :: xs) ys z = z |> fold (f x) ys |> fold_product f xs ys;
-
-(* lists of pairs *)
+(*lists of pairs*)
exception UnequalLengths;
--- a/src/Tools/code/code_target.ML Wed Dec 05 14:15:59 2007 +0100
+++ b/src/Tools/code/code_target.ML Wed Dec 05 14:16:05 2007 +0100
@@ -1037,7 +1037,7 @@
#> fold2 (fn name' => fn base' =>
Graph.new_node (name', (Def (base', NONE)))) names' bases')))
|> apsnd (fold (fn name => fold (add_dep name) deps) names)
- |> apsnd (fold (map_node modl_explode o Graph.add_edge) (product names names))
+ |> apsnd (fold_product (curry (map_node modl_explode o Graph.add_edge)) names names)
end;
fun group_defs [(_, CodeThingol.Bot)] =
I