# HG changeset patch
# User berghofe
# Date 880983750 -3600
# Node ID d4a15e32c0241169e82af870b203e7df4800848e
# Parent  34bb65b037dd298054f3c6bfecceccb81834aaf0
Added DiffCancelSums.

diff -r 34bb65b037dd -r d4a15e32c024 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Mon Dec 01 12:52:18 1997 +0100
+++ b/src/HOL/arith_data.ML	Mon Dec 01 14:42:30 1997 +0100
@@ -123,7 +123,13 @@
 
 (* nat diff *)
 
-(* FIXME *)
+structure DiffCancelSums = CancelSumsFun
+(struct
+  open Sum;
+  val mk_bal = HOLogic.mk_binop "op -";
+  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
+  val uncancel_tac = gen_uncancel_tac diff_cancel;
+end);
 
 
 
@@ -189,11 +195,13 @@
 val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
 val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
 val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
+val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
 
 val nat_cancel_sums = map prep_simproc
   [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
    ("natless_cancel_sums", less_pats, LessCancelSums.proc),
-   ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
+   ("natle_cancel_sums", le_pats, LeCancelSums.proc),
+   ("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
 
 val nat_cancel_factor = map prep_simproc
   [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),