src/HOL/Groebner_Basis.thy
changeset 47432 e1576d13e933
parent 47165 9344891b504b
child 48891 c0eafbd55de3
equal deleted inserted replaced
47431:d9dd4a9f18fc 47432:e1576d13e933
    41 
    41 
    42 setup Algebra_Simplification.setup
    42 setup Algebra_Simplification.setup
    43 
    43 
    44 use "Tools/groebner.ML"
    44 use "Tools/groebner.ML"
    45 
    45 
    46 method_setup algebra = Groebner.algebra_method
    46 method_setup algebra = {*
    47   "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
    47   let
       
    48     fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
       
    49     val addN = "add"
       
    50     val delN = "del"
       
    51     val any_keyword = keyword addN || keyword delN
       
    52     val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
       
    53   in
       
    54     Scan.optional (keyword addN |-- thms) [] --
       
    55      Scan.optional (keyword delN |-- thms) [] >>
       
    56     (fn (add_ths, del_ths) => fn ctxt =>
       
    57       SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
       
    58   end
       
    59 *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
    48 
    60 
    49 declare dvd_def[algebra]
    61 declare dvd_def[algebra]
    50 declare dvd_eq_mod_eq_0[symmetric, algebra]
    62 declare dvd_eq_mod_eq_0[symmetric, algebra]
    51 declare mod_div_trivial[algebra]
    63 declare mod_div_trivial[algebra]
    52 declare mod_mod_trivial[algebra]
    64 declare mod_mod_trivial[algebra]