author chaieb Tue, 12 Jun 2007 10:15:32 +0200 changeset 23332 b91295432e6d parent 23331 da040caa0596 child 23333 ec5b4ab52026
algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts
```--- a/src/HOL/Groebner_Basis.thy	Mon Jun 11 18:34:12 2007 +0200
+++ b/src/HOL/Groebner_Basis.thy	Tue Jun 12 10:15:32 2007 +0200
@@ -4,7 +4,6 @@
*)

header {* Semiring normalization and Groebner Bases *}
-
theory Groebner_Basis
imports NatBin
uses
@@ -14,6 +13,8 @@
("Tools/Groebner_Basis/groebner.ML")
begin

+
+
subsection {* Semiring normalization *}

setup NormalizerData.setup
@@ -436,23 +437,22 @@

use "Tools/Groebner_Basis/groebner.ML"

-ML {*
-  fun algebra_tac ctxt i = ObjectLogic.full_atomize_tac i
-  THEN (fn st =>
-   case try (nth (cprems_of st)) (i - 1) of
-    NONE => no_tac st
-  | SOME p => let val th = Groebner.ring_conv ctxt (Thm.dest_arg p)
-              in rtac th i st end
-              handle TERM _ => no_tac st
-              handle THM _ => no_tac st
-              handle ERROR _ => no_tac st
-              handle CTERM _ => no_tac st);
-*}
+method_setup algebra =
+{*
+let
+ fun keyword k = Scan.lift (Args.\$\$\$ k -- Args.colon) >> K ()
+ val delN = "del"
+ val any_keyword = keyword addN || keyword delN
+ val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+in
+fn src => Method.syntax
+    ((Scan.optional (keyword addN |-- thms) []) --
+    (Scan.optional (keyword delN |-- thms) [])) src
+ #> (fn ((add_ths, del_ths), ctxt) =>
+       Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
+end

-method_setup algebra = {*
-  Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac)
*} ""

-
-
end```