author wenzelm Fri, 26 Nov 2010 20:52:21 +0100 changeset 40718 4d7211968607 parent 40717 88f2955a111e child 40719 acb830207103
eliminated some clones of eq_list;
```--- 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;
```
```--- 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);```