src/HOL/Integ/nat_simprocs.ML

--- a/src/HOL/Integ/nat_simprocs.ML	Sat Jun 16 20:06:42 2001 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Mon Jun 25 15:35:59 2001 +0200
@@ -148,6 +148,9 @@
 
 fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
 
+
+(** Other simproc items **)
+
 val trans_tac = Int_Numeral_Simprocs.trans_tac;
 
 val prove_conv = Int_Numeral_Simprocs.prove_conv;
@@ -159,7 +162,8 @@
                 bin_arith_simps @ bin_rel_simps;
 
 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
+fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
+                                (s, HOLogic.termT);
 val prep_pats = map prep_pat;
 
 
@@ -211,6 +215,23 @@
          mult_0, mult_0_right, mult_1, mult_1_right];
 
 
+(** Restricted version of dest_Sucs_sum for nat_combine_numerals:
+    Simprocs never apply unless the original expression contains at least one
+    numeral in a coefficient position.
+**)
+
+fun is_numeral (Const("Numeral.number_of", _) $ w) = true
+  | is_numeral _ = false;
+
+fun prod_has_numeral t = exists is_numeral (dest_prod t);
+
+fun restricted_dest_Sucs_sum t = 
+  let val ts = dest_Sucs_sum t
+  in  if exists prod_has_numeral ts then ts
+      else raise TERM("Nat_Numeral_Simprocs.restricted_dest_Sucs_sum", ts)
+  end;
+
+
 (*** Applying CancelNumeralsFun ***)
 
 structure CancelNumeralsCommon =
@@ -299,7 +320,7 @@
   struct
   val add		= op + : int*int -> int 
   val mk_sum            = long_mk_sum    (*to work for e.g. #2*x + #3*x *)
-  val dest_sum          = dest_Sucs_sum
+  val dest_sum          = restricted_dest_Sucs_sum
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val left_distrib      = left_add_mult_distrib RS trans