src/HOL/Groebner_Basis.thy
author wenzelm
Fri Mar 07 22:30:58 2014 +0100 (2014-03-07)
changeset 55990 41c6b99c5fb7
parent 55509 bd67ebe275e0
child 56850 13a7bca533a3
permissions -rw-r--r--
more antiquotations;
     1 (*  Title:      HOL/Groebner_Basis.thy
     2     Author:     Amine Chaieb, TU Muenchen
     3 *)
     4 
     5 header {* Groebner bases *}
     6 
     7 theory Groebner_Basis
     8 imports Semiring_Normalization
     9 keywords "try0" :: diag
    10 begin
    11 
    12 subsection {* Groebner Bases *}
    13 
    14 lemmas bool_simps = simp_thms(1-34) -- {* FIXME move to @{theory HOL} *}
    15 
    16 lemma nnf_simps: -- {* FIXME shadows fact binding in @{theory HOL} *}
    17   "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
    18   "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
    19   "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
    20   by blast+
    21 
    22 lemma dnf:
    23   "(P & (Q | R)) = ((P&Q) | (P&R))"
    24   "((Q | R) & P) = ((Q&P) | (R&P))"
    25   "(P \<and> Q) = (Q \<and> P)"
    26   "(P \<or> Q) = (Q \<or> P)"
    27   by blast+
    28 
    29 lemmas weak_dnf_simps = dnf bool_simps
    30 
    31 lemma PFalse:
    32     "P \<equiv> False \<Longrightarrow> \<not> P"
    33     "\<not> P \<Longrightarrow> (P \<equiv> False)"
    34   by auto
    35 
    36 ML {*
    37 structure Algebra_Simplification = Named_Thms
    38 (
    39   val name = @{binding algebra}
    40   val description = "pre-simplification rules for algebraic methods"
    41 )
    42 *}
    43 
    44 setup Algebra_Simplification.setup
    45 
    46 ML_file "Tools/groebner.ML"
    47 
    48 method_setup algebra = {*
    49   let
    50     fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
    51     val addN = "add"
    52     val delN = "del"
    53     val any_keyword = keyword addN || keyword delN
    54     val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    55   in
    56     Scan.optional (keyword addN |-- thms) [] --
    57      Scan.optional (keyword delN |-- thms) [] >>
    58     (fn (add_ths, del_ths) => fn ctxt =>
    59       SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
    60   end
    61 *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
    62 
    63 declare dvd_def[algebra]
    64 declare dvd_eq_mod_eq_0[symmetric, algebra]
    65 declare mod_div_trivial[algebra]
    66 declare mod_mod_trivial[algebra]
    67 declare div_by_0[algebra]
    68 declare mod_by_0[algebra]
    69 declare zmod_zdiv_equality[symmetric,algebra]
    70 declare div_mod_equality2[symmetric, algebra]
    71 declare div_minus_minus[algebra]
    72 declare mod_minus_minus[algebra]
    73 declare div_minus_right[algebra]
    74 declare mod_minus_right[algebra]
    75 declare div_0[algebra]
    76 declare mod_0[algebra]
    77 declare mod_by_1[algebra]
    78 declare div_by_1[algebra]
    79 declare mod_minus1_right[algebra]
    80 declare div_minus1_right[algebra]
    81 declare mod_mult_self2_is_0[algebra]
    82 declare mod_mult_self1_is_0[algebra]
    83 declare zmod_eq_0_iff[algebra]
    84 declare dvd_0_left_iff[algebra]
    85 declare zdvd1_eq[algebra]
    86 declare zmod_eq_dvd_iff[algebra]
    87 declare nat_mod_eq_iff[algebra]
    88 
    89 
    90 subsection {* Try0 *}
    91 
    92 ML_file "Tools/try0.ML"
    93 
    94 end