Added DiffCancelSums.
authorberghofe
Mon Dec 01 14:42:30 1997 +0100 (1997-12-01)
changeset 4332d4a15e32c024
parent 4331 34bb65b037dd
child 4333 1d326b826851
Added DiffCancelSums.
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/arith_data.ML	Mon Dec 01 12:52:18 1997 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Mon Dec 01 14:42:30 1997 +0100
     1.3 @@ -123,7 +123,13 @@
     1.4  
     1.5  (* nat diff *)
     1.6  
     1.7 -(* FIXME *)
     1.8 +structure DiffCancelSums = CancelSumsFun
     1.9 +(struct
    1.10 +  open Sum;
    1.11 +  val mk_bal = HOLogic.mk_binop "op -";
    1.12 +  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
    1.13 +  val uncancel_tac = gen_uncancel_tac diff_cancel;
    1.14 +end);
    1.15  
    1.16  
    1.17  
    1.18 @@ -189,11 +195,13 @@
    1.19  val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
    1.20  val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
    1.21  val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
    1.22 +val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
    1.23  
    1.24  val nat_cancel_sums = map prep_simproc
    1.25    [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
    1.26     ("natless_cancel_sums", less_pats, LessCancelSums.proc),
    1.27 -   ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
    1.28 +   ("natle_cancel_sums", le_pats, LeCancelSums.proc),
    1.29 +   ("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
    1.30  
    1.31  val nat_cancel_factor = map prep_simproc
    1.32    [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),