--- 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;
--- 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 *}
--- 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;
--- 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;