src/HOL/Groebner_Basis.thy
changeset 23332 b91295432e6d
parent 23330 01c09922ce59
child 23389 aaca6a8e5414
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Jun 11 18:34:12 2007 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Jun 12 10:15:32 2007 +0200
     1.3 @@ -4,7 +4,6 @@
     1.4  *)
     1.5  
     1.6  header {* Semiring normalization and Groebner Bases *}
     1.7 -
     1.8  theory Groebner_Basis
     1.9  imports NatBin
    1.10  uses
    1.11 @@ -14,6 +13,8 @@
    1.12    ("Tools/Groebner_Basis/groebner.ML")
    1.13  begin
    1.14  
    1.15 +
    1.16 +
    1.17  subsection {* Semiring normalization *}
    1.18  
    1.19  setup NormalizerData.setup
    1.20 @@ -436,23 +437,22 @@
    1.21  
    1.22  use "Tools/Groebner_Basis/groebner.ML"
    1.23  
    1.24 -ML {*
    1.25 -  fun algebra_tac ctxt i = ObjectLogic.full_atomize_tac i 
    1.26 -  THEN (fn st =>
    1.27 -   case try (nth (cprems_of st)) (i - 1) of
    1.28 -    NONE => no_tac st
    1.29 -  | SOME p => let val th = Groebner.ring_conv ctxt (Thm.dest_arg p)
    1.30 -              in rtac th i st end
    1.31 -              handle TERM _ => no_tac st
    1.32 -              handle THM _ => no_tac st
    1.33 -              handle ERROR _ => no_tac st
    1.34 -              handle CTERM _ => no_tac st);
    1.35 -*}
    1.36 +method_setup algebra =
    1.37 +{* 
    1.38 +let
    1.39 + fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
    1.40 + val addN = "add"
    1.41 + val delN = "del"
    1.42 + val any_keyword = keyword addN || keyword delN
    1.43 + val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    1.44 +in
    1.45 +fn src => Method.syntax 
    1.46 +    ((Scan.optional (keyword addN |-- thms) []) -- 
    1.47 +    (Scan.optional (keyword delN |-- thms) [])) src 
    1.48 + #> (fn ((add_ths, del_ths), ctxt) => 
    1.49 +       Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
    1.50 +end
    1.51  
    1.52 -method_setup algebra = {*
    1.53 -  Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac)
    1.54  *} ""
    1.55  
    1.56 -
    1.57 -
    1.58  end