diff -r bb2250ac9557 -r 0bfd6678a5fa src/Provers/Arith/cancel_numerals.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/Arith/cancel_numerals.ML	Tue Apr 18 15:51:59 2000 +0200
@@ -0,0 +1,61 @@
+(*  Title:      Provers/Arith/cancel_sums.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2000  University of Cambridge
+
+Cancel common literals in balanced expressions:
+
+     i + #m + j ~~ i' + #m' + j'  ==  #(m-m') + i + j ~~ i' + j'
+
+where ~~ is an appropriate balancing operation (e.g. =, <=, <, -).
+*)
+
+signature CANCEL_NUMERALS_DATA =
+sig
+  (*abstract syntax*)
+  val mk_numeral: int -> term
+  val find_first_numeral: term list -> int * term * term list
+  val mk_sum: term list -> term
+  val dest_sum: term -> term list
+  val mk_bal: term * term -> term
+  val dest_bal: term -> term * term
+  (*proof tools*)
+  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
+  val subst_tac: term -> tactic
+  val all_simp_tac: tactic
+end;
+
+signature CANCEL_NUMERALS =
+sig
+  val proc: Sign.sg -> thm list -> term -> thm option
+end;
+
+
+functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
+struct
+
+(*predicting the outputs of other simprocs given a term of the form
+   (i + ... #m + ... j) - #n   *)
+fun cancelled m n terms =
+    if m = n then (*cancel_sums: sort the terms*)
+	sort Term.term_ord terms 
+    else          (*inverse_fold: subtract, keeping original term order*)
+	Data.mk_numeral (m - n) :: terms;
+
+(*the simplification procedure*)
+fun proc sg _ t =
+  let val (t1,t2) = Data.dest_bal t 
+      val (n1, lit1, terms1) = Data.find_first_numeral (Data.dest_sum t1)
+      and (n2, lit2, terms2) = Data.find_first_numeral (Data.dest_sum t2)
+      val lit_n = if n1<n2 then lit1 else lit2
+      and n     = BasisLibrary.Int.min (n1,n2)
+          (*having both the literals and their integer values makes it
+            more robust against negative natural number literals*)
+  in
+      Data.prove_conv [Data.subst_tac lit_n, Data.all_simp_tac] sg
+	 (t, Data.mk_bal (Data.mk_sum (cancelled n1 n terms1),
+			  Data.mk_sum (cancelled n2 n terms2)))
+  end
+  handle _ => None;
+
+end;