# HG changeset patch # User wenzelm # Date 1290801141 -3600 # Node ID 4d72119686073c47dd173f48a4a8c068dfbc089b # Parent 88f2955a111e0971250875b1fc13a0644a9ee718 eliminated some clones of eq_list; diff -r 88f2955a111e -r 4d7211968607 src/HOL/Multivariate_Analysis/normarith.ML --- a/src/HOL/Multivariate_Analysis/normarith.ML Fri Nov 26 18:07:00 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Fri Nov 26 20:52:21 2010 +0100 @@ -117,13 +117,6 @@ [] => [] | h::t => map (cons h) (combinations (k - 1) t) @ combinations k t - -fun forall2 p l1 l2 = case (l1,l2) of - ([],[]) => true - | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2 - | _ => false; - - fun vertices vs eqs = let fun vertex cmb = case solve(vs,cmb) of @@ -131,16 +124,16 @@ | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs) val rawvs = map_filter vertex (combinations (length vs) eqs) val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs - in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset [] + in fold_rev (insert (eq_list op =/)) unset [] end -fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m +val subsumes = eq_list (fn (x, y) => Rat.abs x <=/ Rat.abs y) fun subsume todo dun = case todo of [] => dun |v::ovs => - let val dun' = if exists (fn w => subsumes w v) dun then dun - else v::(filter (fn w => not(subsumes v w)) dun) + let val dun' = if exists (fn w => subsumes (w, v)) dun then dun + else v:: filter (fn w => not (subsumes (v, w))) dun in subsume ovs dun' end; diff -r 88f2955a111e -r 4d7211968607 src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Fri Nov 26 18:07:00 2010 +0100 +++ b/src/HOL/Tools/groebner.ML Fri Nov 26 20:52:21 2010 +0100 @@ -233,14 +233,9 @@ fun align ((p,hp),(q,hq)) = if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp)); -fun forall2 p l1 l2 = - case (l1,l2) of - ([],[]) => true - | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2 - | _ => false; fun poly_eq p1 p2 = - forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2; + eq_list (fn ((c1, m1), (c2, m2)) => c1 =/ c2 andalso (m1: int list) = m2) (p1, p2); fun memx ((p1,h1),(p2,h2)) ppairs = not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);