src/HOL/Tools/nat_arith.ML
changeset 48559 686cc7c47589
parent 48372 868dc809c8a2
child 48560 e0875d956a6b
     1.1 --- a/src/HOL/Tools/nat_arith.ML	Fri Jul 27 17:34:33 2012 +0200
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Fri Jul 27 17:57:31 2012 +0200
     1.3 @@ -8,10 +8,10 @@
     1.4    val mk_sum: term list -> term
     1.5    val mk_norm_sum: term list -> term
     1.6    val dest_sum: term -> term list
     1.7 -
     1.8 -  val nat_cancel_sums_add: simproc list
     1.9 -  val nat_cancel_sums: simproc list
    1.10 -  val setup: Context.generic -> Context.generic
    1.11 +  val nateq_cancel_sums: simpset -> cterm -> thm option
    1.12 +  val natless_cancel_sums: simpset -> cterm -> thm option
    1.13 +  val natle_cancel_sums: simpset -> cterm -> thm option
    1.14 +  val natdiff_cancel_sums: simpset -> cterm -> thm option
    1.15  end;
    1.16  
    1.17  structure Nat_Arith: NAT_ARITH =
    1.18 @@ -88,23 +88,9 @@
    1.19    val cancel_rule = mk_meta_eq @{thm diff_cancel};
    1.20  end);
    1.21  
    1.22 -val nat_cancel_sums_add =
    1.23 -  [Simplifier.simproc_global @{theory} "nateq_cancel_sums"
    1.24 -     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
    1.25 -     (K EqCancelSums.proc),
    1.26 -   Simplifier.simproc_global @{theory} "natless_cancel_sums"
    1.27 -     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
    1.28 -     (K LessCancelSums.proc),
    1.29 -   Simplifier.simproc_global @{theory} "natle_cancel_sums"
    1.30 -     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
    1.31 -     (K LeCancelSums.proc)];
    1.32 -
    1.33 -val nat_cancel_sums = nat_cancel_sums_add @
    1.34 -  [Simplifier.simproc_global @{theory} "natdiff_cancel_sums"
    1.35 -    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
    1.36 -    (K DiffCancelSums.proc)];
    1.37 -
    1.38 -val setup =
    1.39 -  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
    1.40 +fun nateq_cancel_sums ss = EqCancelSums.proc ss o Thm.term_of
    1.41 +fun natless_cancel_sums ss = LessCancelSums.proc ss o Thm.term_of
    1.42 +fun natle_cancel_sums ss = LeCancelSums.proc ss o Thm.term_of
    1.43 +fun natdiff_cancel_sums ss = DiffCancelSums.proc ss o Thm.term_of
    1.44  
    1.45  end;