uniform use of Integer.add/mult/sum/prod;

--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -223,7 +223,7 @@
 fun monomial_var x = FuncUtil.Ctermfunc.onefunc (x, 1);
 
 val monomial_mul =
-  FuncUtil.Ctermfunc.combine (curry op +) (K false);
+  FuncUtil.Ctermfunc.combine Integer.add (K false);
 
 fun monomial_pow m k =
   if k = 0 then monomial_1
@@ -233,7 +233,7 @@
   FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => FuncUtil.Ctermfunc.tryapplyd m2 x 0 >= k andalso a) m1 true;;
 
 fun monomial_div m1 m2 =
- let val m = FuncUtil.Ctermfunc.combine (curry op +)
+ let val m = FuncUtil.Ctermfunc.combine Integer.add
    (fn x => x = 0) m1 (FuncUtil.Ctermfunc.map (fn x => ~ x) m2)
  in if FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k >= 0 andalso a) m true then m
   else error "monomial_div: non-divisible"

--- a/src/HOL/Library/positivstellensatz.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -83,8 +83,8 @@
  else
   let val mon1 = dest_monomial m1 
       val mon2 = dest_monomial m2
-      val deg1 = fold (curry op + o snd) mon1 0
-      val deg2 = fold (curry op + o snd) mon2 0 
+      val deg1 = fold (Integer.add o snd) mon1 0
+      val deg2 = fold (Integer.add o snd) mon2 0 
   in if deg1 < deg2 then GREATER else if deg1 > deg2 then LESS
      else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2)
   end;

--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -22,7 +22,7 @@
     val (_, _, constrs) = the (AList.lookup (op =) descr i);
     fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
           then NONE
-          else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i)
+          else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i)
       | arg_nonempty _ = SOME 0;
     fun max xs = Library.foldl
       (fn (NONE, _) => NONE

--- a/src/HOL/Tools/Function/fundef_datatype.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_datatype.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -54,7 +54,7 @@
       val _ = map check_constr_pattern args
                   
                   (* just count occurrences to check linearity *)
-      val _ = if fold (fold_aterms (fn Bound _ => curry (op +) 1 | _ => I)) args 0 > length qs
+      val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs
               then err "Nonlinear patterns" else ()
     in
       ()

--- a/src/HOL/Tools/Function/scnp_solve.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -46,7 +46,7 @@
 fun num_prog_pts (GP (arities, _)) = length arities ;
 fun num_graphs (GP (_, gs)) = length gs ;
 fun arity (GP (arities, gl)) i = nth arities i ;
-fun ndigits (GP (arities, _)) = IntInf.log2 (List.foldl (op +) 0 arities) + 1
+fun ndigits (GP (arities, _)) = IntInf.log2 (Integer.sum arities) + 1
 
 
 (** Propositional formulas **)

--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -391,8 +391,8 @@
  in fn tm1 => fn tm2 =>
   let val vdegs1 = map dest_varpow (powervars tm1)
       val vdegs2 = map dest_varpow (powervars tm2)
-      val deg1 = fold_rev ((curry (op +)) o snd) vdegs1 num_0
-      val deg2 = fold_rev ((curry (op +)) o snd) vdegs2 num_0
+      val deg1 = fold (Integer.add o snd) vdegs1 num_0
+      val deg2 = fold (Integer.add o snd) vdegs2 num_0
   in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
                             else lexorder vdegs1 vdegs2
   end

--- a/src/HOL/Tools/Qelim/cooper.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -188,7 +188,7 @@
     (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1,
     Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
    if x1 = x2 then
-     let val c = numeral2 (curry op +) c1 c2
+     let val c = numeral2 Integer.add c1 c2
       in if c = zero then linear_add vars r1 r2
          else addC$(mulC$c$x1)$(linear_add vars r1 r2)
      end
@@ -198,7 +198,7 @@
       addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
  | (_, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
       addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
- | (_, _) => numeral2 (curry op +) tm1 tm2;
+ | (_, _) => numeral2 Integer.add tm1 tm2;
 
 fun linear_neg tm = linear_cmul ~1 tm;
 fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);

--- a/src/HOL/Tools/refute.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/HOL/Tools/refute.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -1616,30 +1616,14 @@
   end;
 
 (* ------------------------------------------------------------------------- *)
-(* sum: returns the sum of a list 'xs' of integers                           *)
-(* ------------------------------------------------------------------------- *)
-
-  (* int list -> int *)
-
-  fun sum xs = List.foldl op+ 0 xs;
-
-(* ------------------------------------------------------------------------- *)
-(* product: returns the product of a list 'xs' of integers                   *)
-(* ------------------------------------------------------------------------- *)
-
-  (* int list -> int *)
-
-  fun product xs = List.foldl op* 1 xs;
-
-(* ------------------------------------------------------------------------- *)
 (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *)
 (*               is the sum (over its constructors) of the product (over     *)
 (*               their arguments) of the size of the argument types          *)
 (* ------------------------------------------------------------------------- *)
 
   fun size_of_dtyp thy typ_sizes descr typ_assoc constructors =
-    sum (map (fn (_, dtyps) =>
-      product (map (size_of_type thy (typ_sizes, []) o
+    Integer.sum (map (fn (_, dtyps) =>
+      Integer.prod (map (size_of_type thy (typ_sizes, []) o
         (typ_of_dtyp descr typ_assoc)) dtyps))
           constructors);
 
@@ -2326,8 +2310,8 @@
             let
               (* number of all constructors, including those of different  *)
               (* (mutually recursive) datatypes within the same descriptor *)
-              val mconstrs_count = sum (map (fn (_, (_, _, cs)) => length cs)
-                (#descr info))
+              val mconstrs_count =
+                Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info))
             in
               if mconstrs_count < length params then
                 (* too many actual parameters; for now we'll use the *)

--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -301,14 +301,14 @@
   if n = 1 then i
   else if n = 0 andalso ty = Lt then sys_error "multiply_ineq"
   else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq"
-  else Lineq (n * k, ty, map (curry op* n) l, Multiplied (n, just));
+  else Lineq (n * k, ty, map (Integer.mult n) l, Multiplied (n, just));
 
 (* ------------------------------------------------------------------------- *)
 (* Add together (in)equations.                                               *)
 (* ------------------------------------------------------------------------- *)
 
 fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
-  let val l = map2 (curry (op +)) l1 l2
+  let val l = map2 Integer.add l1 l2
   in Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) end;
 
 (* ------------------------------------------------------------------------- *)

--- a/src/Pure/General/integer.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/Pure/General/integer.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -1,13 +1,16 @@
 (*  Title:      Pure/General/integer.ML
     Author:     Florian Haftmann, TU Muenchen
 
-Unbounded integers.
+Auxiliary operations on (unbounded) integers.
 *)
 
 signature INTEGER =
 sig
+  val add: int -> int -> int
+  val mult: int -> int -> int
+  val sum: int list -> int
+  val prod: int list -> int
   val sign: int -> order
-  val sum: int list -> int
   val div_mod: int -> int -> int * int
   val square: int -> int
   val pow: int -> int -> int (* exponent -> base -> result *)
@@ -20,9 +23,13 @@
 structure Integer : INTEGER =
 struct
 
-fun sign x = int_ord (x, 0);
+fun add x y = x + y;
+fun mult x y = x * y;
 
-fun sum xs = fold (curry op +) xs 0;
+fun sum xs = fold add xs 0;
+fun prod xs = fold mult xs 1;
+
+fun sign x = int_ord (x, 0);
 
 fun div_mod x y = IntInf.divMod (x, y);
 

--- a/src/Tools/atomize_elim.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/Tools/atomize_elim.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -42,7 +42,7 @@
 (* rearrange_prems as a conversion *)
 fun rearrange_prems_conv pi ct =
     let
-      val pi' = 0 :: map (curry op + 1) pi
+      val pi' = 0 :: map (Integer.add 1) pi
       val fwd  = Thm.trivial ct
                   |> Drule.rearrange_prems pi'
       val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd)))

--- a/src/Tools/nbe.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/Tools/nbe.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -303,7 +303,7 @@
     fun subst_nonlin_vars args =
       let
         val vs = (fold o Code_Thingol.fold_varnames)
-          (fn v => AList.map_default (op =) (v, 0) (curry (op +) 1)) args [];
+          (fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args [];
         val names = Name.make_context (map fst vs);
         fun declare v k ctxt = let val vs = Name.invents ctxt v k
           in (vs, fold Name.declare vs ctxt) end;