1 (* Title: HOL/Groebner_Basis.thy
2 Author: Amine Chaieb, TU Muenchen
5 header {* Groebner bases *}
8 imports Semiring_Normalization
13 subsection {* Groebner Bases *}
15 lemmas bool_simps = simp_thms(1-34)
18 "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
19 "(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"
22 lemmas weak_dnf_simps = dnf bool_simps
25 "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
26 "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
30 "P \<equiv> False \<Longrightarrow> \<not> P"
31 "\<not> P \<Longrightarrow> (P \<equiv> False)"
35 structure Algebra_Simplification = Named_Thms
37 val name = @{binding algebra}
38 val description = "pre-simplification rules for algebraic methods"
42 setup Algebra_Simplification.setup
44 use "Tools/groebner.ML"
46 method_setup algebra = Groebner.algebra_method
47 "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
49 declare dvd_def[algebra]
50 declare dvd_eq_mod_eq_0[symmetric, algebra]
51 declare mod_div_trivial[algebra]
52 declare mod_mod_trivial[algebra]
53 declare div_by_0[algebra]
54 declare mod_by_0[algebra]
55 declare zmod_zdiv_equality[symmetric,algebra]
56 declare zdiv_zmod_equality[symmetric, algebra]
57 declare zdiv_zminus_zminus[algebra]
58 declare zmod_zminus_zminus[algebra]
59 declare zdiv_zminus2[algebra]
60 declare zmod_zminus2[algebra]
61 declare div_0[algebra]
62 declare mod_0[algebra]
63 declare mod_by_1[algebra]
64 declare div_by_1[algebra]
65 declare zmod_minus1_right[algebra]
66 declare zdiv_minus1_right[algebra]
67 declare mod_div_trivial[algebra]
68 declare mod_mod_trivial[algebra]
69 declare mod_mult_self2_is_0[algebra]
70 declare mod_mult_self1_is_0[algebra]
71 declare zmod_eq_0_iff[algebra]
72 declare dvd_0_left_iff[algebra]
73 declare zdvd1_eq[algebra]
74 declare zmod_eq_dvd_iff[algebra]
75 declare nat_mod_eq_iff[algebra]