# HG changeset patch
# User haftmann
# Date 1256907591 -3600
# Node ID 8b673ae1bf39506eda5212ce73e211d51eb43624
# Parent  3495dbba0da2061fac8ec16a19d2d4ea7708c612
dedicated theory for loading numeral simprocs

diff -r 3495dbba0da2 -r 8b673ae1bf39 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Fri Oct 30 13:59:51 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML	Fri Oct 30 13:59:51 2009 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Tools/arith_data.ML
     Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
 
-Common arithmetic proof auxiliary.
+Common arithmetic proof auxiliary and legacy.
 *)
 
 signature ARITH_DATA =
@@ -11,6 +11,11 @@
   val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
   val get_arith_facts: Proof.context -> thm list
 
+  val mk_number: typ -> int -> term
+  val mk_sum: typ -> term list -> term
+  val long_mk_sum: typ -> term list -> term
+  val dest_sum: term -> term list
+
   val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
   val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
@@ -67,6 +72,36 @@
     "various arithmetic decision procedures";
 
 
+(* some specialized syntactic operations *)
+
+fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
+
+val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
+
+fun mk_minus t = 
+  let val T = Term.fastype_of t
+  in Const (@{const_name HOL.uminus}, T --> T) $ t end;
+
+(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
+fun mk_sum T []        = mk_number T 0
+  | mk_sum T [t,u]     = mk_plus (t, u)
+  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
+
+(*this version ALWAYS includes a trailing zero*)
+fun long_mk_sum T []        = mk_number T 0
+  | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
+
+(*decompose additions AND subtractions as a sum*)
+fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) =
+        dest_summing (pos, t, dest_summing (pos, u, ts))
+  | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) =
+        dest_summing (pos, t, dest_summing (not pos, u, ts))
+  | dest_summing (pos, t, ts) =
+        if pos then t::ts else mk_minus t :: ts;
+
+fun dest_sum t = dest_summing (true, t, []);
+
+
 (* various auxiliary and legacy *)
 
 fun prove_conv_nohyps tacs ctxt (t, u) =
diff -r 3495dbba0da2 -r 8b673ae1bf39 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Fri Oct 30 13:59:51 2009 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Oct 30 13:59:51 2009 +0100
@@ -16,9 +16,6 @@
 
 signature NUMERAL_SIMPROCS =
 sig
-  val mk_sum: typ -> term list -> term
-  val dest_sum: term -> term list
-
   val assoc_fold_simproc: simproc
   val combine_numerals: simproc
   val cancel_numerals: simproc list
@@ -32,39 +29,10 @@
 structure Numeral_Simprocs : NUMERAL_SIMPROCS =
 struct
 
-fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
-
-fun find_first_numeral past (t::terms) =
-        ((snd (HOLogic.dest_number t), rev past @ terms)
-         handle TERM _ => find_first_numeral (t::past) terms)
-  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
-
-val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
-
-fun mk_minus t = 
-  let val T = Term.fastype_of t
-  in Const (@{const_name HOL.uminus}, T --> T) $ t end;
-
-(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
-fun mk_sum T []        = mk_number T 0
-  | mk_sum T [t,u]     = mk_plus (t, u)
-  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
-
-(*this version ALWAYS includes a trailing zero*)
-fun long_mk_sum T []        = mk_number T 0
-  | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
-
-val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT;
-
-(*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) =
-        dest_summing (pos, t, dest_summing (pos, u, ts))
-  | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) =
-        dest_summing (pos, t, dest_summing (not pos, u, ts))
-  | dest_summing (pos, t, ts) =
-        if pos then t::ts else mk_minus t :: ts;
-
-fun dest_sum t = dest_summing (true, t, []);
+val mk_number = Arith_Data.mk_number;
+val mk_sum = Arith_Data.mk_sum;
+val long_mk_sum = Arith_Data.long_mk_sum;
+val dest_sum = Arith_Data.dest_sum;
 
 val mk_diff = HOLogic.mk_binop @{const_name HOL.minus};
 val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT;
@@ -95,6 +63,11 @@
       in dest_prod t @ dest_prod u end
       handle TERM _ => [t];
 
+fun find_first_numeral past (t::terms) =
+        ((snd (HOLogic.dest_number t), rev past @ terms)
+         handle TERM _ => find_first_numeral (t::past) terms)
+  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
+
 (*DON'T do the obvious simplifications; that would create special cases*)
 fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);