src/HOL/Tools/arith_data.ML

--- a/src/HOL/Tools/arith_data.ML	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML	Mon Mar 23 19:01:16 2009 +0100
@@ -6,6 +6,11 @@
 
 signature ARITH_DATA =
 sig
+  val arith_tac: Proof.context -> int -> tactic
+  val verbose_arith_tac: Proof.context -> int -> tactic
+  val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
+  val get_arith_facts: Proof.context -> thm 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
@@ -14,11 +19,54 @@
   val trans_tac: thm option -> tactic
   val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
     -> simproc
+
+  val setup: theory -> theory
 end;
 
 structure Arith_Data: ARITH_DATA =
 struct
 
+(* slots for pluging in arithmetic facts and tactics *)
+
+structure Arith_Facts = NamedThmsFun(
+  val name = "arith"
+  val description = "arith facts - only ground formulas"
+);
+
+val get_arith_facts = Arith_Facts.get;
+
+structure Arith_Tactics = TheoryDataFun
+(
+  type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
+  val empty = [];
+  val copy = I;
+  val extend = I;
+  fun merge _ = AList.merge (op =) (K true);
+);
+
+fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
+
+fun gen_arith_tac verbose ctxt =
+  let
+    val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt
+    fun invoke (_, (name, tac)) k st = (if verbose
+      then warning ("Trying " ^ name ^ "...") else ();
+      tac verbose ctxt k st);
+  in FIRST' (map invoke (rev tactics)) end;
+
+val arith_tac = gen_arith_tac false;
+val verbose_arith_tac = gen_arith_tac true;
+
+val arith_method = Args.bang_facts >> (fn prems => fn ctxt =>
+  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
+    THEN' verbose_arith_tac ctxt)));
+
+val setup = Arith_Facts.setup
+  #> Method.setup @{binding arith} arith_method "various arithmetic decision procedures";
+
+
+(* various auxiliary and legacy *)
+
 fun prove_conv_nohyps tacs ctxt (t, u) =
   if t aconv u then NONE
   else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))