# HG changeset patch
# User haftmann
# Date 1203515558 -3600
# Node ID a657683e902af6b700f840c2606d20bdf45fcb3f
# Parent  fbc60cd02ae230acb896e7485030857d2430a4b9
tuned structures in arith_data.ML

diff -r fbc60cd02ae2 -r a657683e902a src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Wed Feb 20 14:52:34 2008 +0100
+++ b/src/HOL/IntDiv.thy	Wed Feb 20 14:52:38 2008 +0100
@@ -274,13 +274,13 @@
   val prove_eq_sums =
     let
       val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
-    in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
+    in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
 end)
 
 in
 
-val cancel_zdiv_zmod_proc = NatArithUtils.prep_simproc
-  ("cancel_zdiv_zmod", ["(m::int) + n"], K CancelDivMod.proc)
+val cancel_zdiv_zmod_proc = Simplifier.simproc @{theory}
+  "cancel_zdiv_zmod" ["(m::int) + n"] (K CancelDivMod.proc)
 
 end;
 
diff -r fbc60cd02ae2 -r a657683e902a src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Feb 20 14:52:34 2008 +0100
+++ b/src/HOL/Nat.thy	Wed Feb 20 14:52:38 2008 +0100
@@ -1199,7 +1199,7 @@
   using 2 1 by (rule trans)
 
 use "arith_data.ML"
-declaration {* K arith_data_setup *}
+declaration {* K ArithData.setup *}
 
 use "Tools/lin_arith.ML"
 declaration {* K LinArith.setup *}
diff -r fbc60cd02ae2 -r a657683e902a src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Wed Feb 20 14:52:34 2008 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Wed Feb 20 14:52:38 2008 +0100
@@ -810,7 +810,7 @@
         @{thm "not_one_less_zero"}]
       addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
        (*abel_cancel helps it work in abstract algebraic domains*)
-      addsimprocs nat_cancel_sums_add}) #>
+      addsimprocs ArithData.nat_cancel_sums_add}) #>
   arith_discrete "nat";
 
 val lin_arith_simproc = Fast_Arith.lin_arith_simproc;
diff -r fbc60cd02ae2 -r a657683e902a src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Feb 20 14:52:34 2008 +0100
+++ b/src/HOL/arith_data.ML	Wed Feb 20 14:52:38 2008 +0100
@@ -5,16 +5,48 @@
 Basic arithmetic proof tools.
 *)
 
-(*** cancellation of common terms ***)
+signature ARITH_DATA =
+sig
+  val prove_conv: tactic -> (MetaSimplifier.simpset -> tactic)
+    -> MetaSimplifier.simpset -> term * term -> thm
+  val simp_all_tac: thm list -> MetaSimplifier.simpset -> tactic
+
+  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
+end;
 
-structure NatArithUtils =
+structure ArithData: ARITH_DATA =
 struct
 
+(** generic proof tools **)
+
+(* prove conversions *)
+
+fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
+  mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
+      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
+    (K (EVERY [expand_tac, norm_tac ss]))));
+
+(* rewriting *)
+
+fun simp_all_tac rules =
+  let val ss0 = HOL_ss addsimps rules
+  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
+
+
 (** abstract syntax of structure nat: 0, Suc, + **)
 
-(* mk_sum, mk_norm_sum *)
+local
 
 val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
+val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
+
+in
 
 fun mk_sum [] = HOLogic.zero
   | mk_sum [t] = t
@@ -27,10 +59,6 @@
   end;
 
 
-(* dest_sum *)
-
-val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
-
 fun dest_sum tm =
   if HOLogic.is_zero tm then []
   else
@@ -41,46 +69,9 @@
           SOME (t, u) => dest_sum t @ dest_sum u
         | NONE => [tm]));
 
-
-
-(** generic proof tools **)
-
-(* prove conversions *)
-
-fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
-  mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
-      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
-    (K (EVERY [expand_tac, norm_tac ss]))));
-
-
-(* rewriting *)
-
-fun simp_all_tac rules =
-  let val ss0 = HOL_ss addsimps rules
-  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
-
-fun prep_simproc (name, pats, proc) =
-  Simplifier.simproc (the_context ()) name pats proc;
-
 end;
 
 
-
-(** ArithData **)
-
-signature ARITH_DATA =
-sig
-  val nat_cancel_sums_add: simproc list
-  val nat_cancel_sums: simproc list
-  val arith_data_setup: Context.generic -> Context.generic
-end;
-
-structure ArithData: ARITH_DATA =
-struct
-
-open NatArithUtils;
-
-
 (** cancel common summands **)
 
 structure Sum =
@@ -144,25 +135,23 @@
 
 (* prepare nat_cancel simprocs *)
 
-val nat_cancel_sums_add = map prep_simproc
-  [("nateq_cancel_sums",
-     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"],
-     K EqCancelSums.proc),
-   ("natless_cancel_sums",
-     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"],
-     K LessCancelSums.proc),
-   ("natle_cancel_sums",
-     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"],
-     K LeCancelSums.proc)];
+val nat_cancel_sums_add =
+  [Simplifier.simproc @{theory} "nateq_cancel_sums"
+     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
+     (K EqCancelSums.proc),
+   Simplifier.simproc @{theory} "natless_cancel_sums"
+     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
+     (K LessCancelSums.proc),
+   Simplifier.simproc @{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 @
-  [prep_simproc ("natdiff_cancel_sums",
-    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"],
-    K DiffCancelSums.proc)];
+  [Simplifier.simproc @{theory} "natdiff_cancel_sums"
+    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
+    (K DiffCancelSums.proc)];
 
-val arith_data_setup =
+val setup =
   Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
 
 end;
-
-open ArithData;