1(*  Title:      HOL/Groebner_Basis.thy
2    Author:     Amine Chaieb, TU Muenchen
3*)
4
5section \<open>Groebner bases\<close>
6
7theory Groebner_Basis
8imports Semiring_Normalization Parity
9begin
10
11subsection \<open>Groebner Bases\<close>
12
13lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to @{theory HOL.HOL}\<close>
14
15lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in @{theory HOL.HOL}\<close>
16  "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
17  "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
18  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
19  by blast+
20
21lemma dnf:
22  "(P \<and> (Q \<or> R)) = ((P\<and>Q) \<or> (P\<and>R))"
23  "((Q \<or> R) \<and> P) = ((Q\<and>P) \<or> (R\<and>P))"
24  "(P \<and> Q) = (Q \<and> P)"
25  "(P \<or> Q) = (Q \<or> P)"
26  by blast+
27
28lemmas weak_dnf_simps = dnf bool_simps
29
30lemma PFalse:
31    "P \<equiv> False \<Longrightarrow> \<not> P"
32    "\<not> P \<Longrightarrow> (P \<equiv> False)"
33  by auto
34
35named_theorems algebra "pre-simplification rules for algebraic methods"
36ML_file "Tools/groebner.ML"
37
38method_setup algebra = \<open>
39  let
40    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
41    val addN = "add"
42    val delN = "del"
43    val any_keyword = keyword addN || keyword delN
44    val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
45  in
46    Scan.optional (keyword addN |-- thms) [] --
47     Scan.optional (keyword delN |-- thms) [] >>
48    (fn (add_ths, del_ths) => fn ctxt =>
49      SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
50  end
51\<close> "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
52
53declare dvd_def[algebra]
54declare mod_eq_0_iff_dvd[algebra]
55declare mod_div_trivial[algebra]
56declare mod_mod_trivial[algebra]
57declare div_by_0[algebra]
58declare mod_by_0[algebra]
59declare mult_div_mod_eq[algebra]
60declare div_minus_minus[algebra]
61declare mod_minus_minus[algebra]
62declare div_minus_right[algebra]
63declare mod_minus_right[algebra]
64declare div_0[algebra]
65declare mod_0[algebra]
66declare mod_by_1[algebra]
67declare div_by_1[algebra]
68declare mod_minus1_right[algebra]
69declare div_minus1_right[algebra]
70declare mod_mult_self2_is_0[algebra]
71declare mod_mult_self1_is_0[algebra]
72declare zmod_eq_0_iff[algebra]
73declare dvd_0_left_iff[algebra]
74declare zdvd1_eq[algebra]
75declare mod_eq_dvd_iff[algebra]
76declare nat_mod_eq_iff[algebra]
77
78context semiring_parity
79begin
80
81declare even_mult_iff [algebra]
82declare even_power [algebra]
83
84end
85
86context ring_parity
87begin
88
89declare even_minus [algebra]
90
91end
92
93declare even_Suc [algebra]
94declare even_diff_nat [algebra]
95
96end
97