# HG changeset patch
# User huffman
# Date 1179767137 -7200
# Node ID c722004c5a2239781a1884d05151a7d3e781dd62
# Parent  68b152e8ea86be69b2b1d5cc7b2a3dfe40a7f463
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int

diff -r 68b152e8ea86 -r c722004c5a22 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Mon May 21 18:53:04 2007 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Mon May 21 19:05:37 2007 +0200
@@ -383,6 +383,8 @@
 
 structure CombineNumeralsData =
   struct
+  type coeff            = IntInf.int
+  val iszero            = (fn x => x = 0)
   val add               = IntInf.+ 
   val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   val dest_sum          = dest_sum
diff -r 68b152e8ea86 -r c722004c5a22 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Mon May 21 18:53:04 2007 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Mon May 21 19:05:37 2007 +0200
@@ -234,6 +234,8 @@
 
 structure CombineNumeralsData =
   struct
+  type coeff            = IntInf.int
+  val iszero            = (fn x => x = 0)
   val add               = IntInf.+
   val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
   val dest_sum          = dest_Sucs_sum false
diff -r 68b152e8ea86 -r c722004c5a22 src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Mon May 21 18:53:04 2007 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Mon May 21 19:05:37 2007 +0200
@@ -19,11 +19,13 @@
 signature COMBINE_NUMERALS_DATA =
 sig
   (*abstract syntax*)
-  val add: IntInf.int * IntInf.int -> IntInf.int     (*addition (or multiplication) *)
+  eqtype coeff
+  val iszero: coeff -> bool
+  val add: coeff * coeff -> coeff     (*addition (or multiplication) *)
   val mk_sum: typ -> term list -> term
   val dest_sum: term -> term list
-  val mk_coeff: IntInf.int * term -> term
-  val dest_coeff: term -> IntInf.int * term
+  val mk_coeff: coeff * term -> term
+  val dest_coeff: term -> coeff * term
   (*rules*)
   val left_distrib: thm
   (*proof tools*)
@@ -75,7 +77,7 @@
 
     val reshape =  (*Move i*u to the front and put j*u into standard form
                        i + #m + j + k == #m + i + (j + k) *)
-      if m=0 orelse n=0 then   (*trivial, so do nothing*)
+      if Data.iszero m orelse Data.iszero n then   (*trivial, so do nothing*)
         raise TERM("combine_numerals", [])
       else Data.prove_conv [Data.norm_tac ss] ctxt
         (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms))