# HG changeset patch
# User huffman
# Date 1343404651 -7200
# Node ID 686cc7c4758955aee74ac6638900501fb358490c
# Parent  fabbed3abc1eee9e04b97a1e740b9c51c24695be
give Nat_Arith simprocs proper name bindings by using simproc_setup

diff -r fabbed3abc1e -r 686cc7c47589 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Jul 27 17:34:33 2012 +0200
+++ b/src/HOL/Nat.thy	Fri Jul 27 17:57:31 2012 +0200
@@ -1494,7 +1494,22 @@
 setup Arith_Data.setup
 
 use "Tools/nat_arith.ML"
-declaration {* K Nat_Arith.setup *}
+
+simproc_setup nateq_cancel_sums
+  ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
+  {* fn phi => Nat_Arith.nateq_cancel_sums *}
+
+simproc_setup natless_cancel_sums
+  ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
+  {* fn phi => Nat_Arith.natless_cancel_sums *}
+
+simproc_setup natle_cancel_sums
+  ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
+  {* fn phi => Nat_Arith.natle_cancel_sums *}
+
+simproc_setup natdiff_cancel_sums
+  ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
+  {* fn phi => Nat_Arith.natdiff_cancel_sums *}
 
 use "Tools/lin_arith.ML"
 setup {* Lin_Arith.global_setup *}
diff -r fabbed3abc1e -r 686cc7c47589 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Jul 27 17:34:33 2012 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Fri Jul 27 17:57:31 2012 +0200
@@ -815,7 +815,9 @@
                    @{simproc group_cancel_eq}, @{simproc group_cancel_le},
                    @{simproc group_cancel_less}]
        (*abel_cancel helps it work in abstract algebraic domains*)
-      addsimprocs Nat_Arith.nat_cancel_sums_add
+      addsimprocs [@{simproc nateq_cancel_sums},
+                   @{simproc natless_cancel_sums},
+                   @{simproc natle_cancel_sums}]
       |> Simplifier.add_cong @{thm if_weak_cong},
     number_of = number_of}) #>
   add_discrete_type @{type_name nat};
diff -r fabbed3abc1e -r 686cc7c47589 src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Fri Jul 27 17:34:33 2012 +0200
+++ b/src/HOL/Tools/nat_arith.ML	Fri Jul 27 17:57:31 2012 +0200
@@ -8,10 +8,10 @@
   val mk_sum: term list -> term
   val mk_norm_sum: term list -> term
   val dest_sum: term -> term list
-
-  val nat_cancel_sums_add: simproc list
-  val nat_cancel_sums: simproc list
-  val setup: Context.generic -> Context.generic
+  val nateq_cancel_sums: simpset -> cterm -> thm option
+  val natless_cancel_sums: simpset -> cterm -> thm option
+  val natle_cancel_sums: simpset -> cterm -> thm option
+  val natdiff_cancel_sums: simpset -> cterm -> thm option
 end;
 
 structure Nat_Arith: NAT_ARITH =
@@ -88,23 +88,9 @@
   val cancel_rule = mk_meta_eq @{thm diff_cancel};
 end);
 
-val nat_cancel_sums_add =
-  [Simplifier.simproc_global @{theory} "nateq_cancel_sums"
-     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
-     (K EqCancelSums.proc),
-   Simplifier.simproc_global @{theory} "natless_cancel_sums"
-     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
-     (K LessCancelSums.proc),
-   Simplifier.simproc_global @{theory} "natle_cancel_sums"
-     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
-     (K LeCancelSums.proc)];
-
-val nat_cancel_sums = nat_cancel_sums_add @
-  [Simplifier.simproc_global @{theory} "natdiff_cancel_sums"
-    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
-    (K DiffCancelSums.proc)];
-
-val setup =
-  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
+fun nateq_cancel_sums ss = EqCancelSums.proc ss o Thm.term_of
+fun natless_cancel_sums ss = LessCancelSums.proc ss o Thm.term_of
+fun natle_cancel_sums ss = LeCancelSums.proc ss o Thm.term_of
+fun natdiff_cancel_sums ss = DiffCancelSums.proc ss o Thm.term_of
 
 end;
diff -r fabbed3abc1e -r 686cc7c47589 src/HOL/ex/Simproc_Tests.thy
--- a/src/HOL/ex/Simproc_Tests.thy	Fri Jul 27 17:34:33 2012 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy	Fri Jul 27 17:57:31 2012 +0200
@@ -27,21 +27,21 @@
   fix a b c d :: nat
   {
     assume "b = Suc c" have "a + b = Suc (c + a)"
-      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 0] *}) fact
+      by (tactic {* test [@{simproc nateq_cancel_sums}] *}) fact
   next
     assume "b < Suc c" have "a + b < Suc (c + a)"
-      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 1] *}) fact
+      by (tactic {* test [@{simproc natless_cancel_sums}] *}) fact
   next
     assume "b \<le> Suc c" have "a + b \<le> Suc (c + a)"
-      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 2] *}) fact
+      by (tactic {* test [@{simproc natle_cancel_sums}] *}) fact
   next
     assume "b - Suc c = d" have "a + b - Suc (c + a) = d"
-      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 3] *}) fact
+      by (tactic {* test [@{simproc natdiff_cancel_sums}] *}) fact
   }
 end
 
 schematic_lemma "\<And>(y::?'b::size). size (?x::?'a::size) \<le> size y + size ?x"
-  by (tactic {* test [nth Nat_Arith.nat_cancel_sums 2] *}) (rule le0)
+  by (tactic {* test [@{simproc natle_cancel_sums}] *}) (rule le0)
 (* TODO: test more simprocs with schematic variables *)
 
 subsection {* Abelian group cancellation simprocs *}