wenzelm@23252: (*  Title:      HOL/Groebner_Basis.thy
wenzelm@23252:     Author:     Amine Chaieb, TU Muenchen
wenzelm@23252: *)
wenzelm@23252: 
haftmann@36751: header {* Groebner bases *}
haftmann@28402: 
wenzelm@23252: theory Groebner_Basis
haftmann@36751: imports Semiring_Normalization
wenzelm@23252: begin
wenzelm@23252: 
haftmann@36712: subsection {* Groebner Bases *}
haftmann@36712: 
haftmann@36712: lemmas bool_simps = simp_thms(1-34)
haftmann@36712: 
haftmann@36712: lemma dnf:
haftmann@36712:     "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
haftmann@36712:     "(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"
haftmann@36712:   by blast+
haftmann@36712: 
haftmann@36712: lemmas weak_dnf_simps = dnf bool_simps
haftmann@36712: 
haftmann@36712: lemma nnf_simps:
haftmann@36712:     "(\<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)"
haftmann@36712:     "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
haftmann@36712:   by blast+
haftmann@36712: 
haftmann@36712: lemma PFalse:
haftmann@36712:     "P \<equiv> False \<Longrightarrow> \<not> P"
haftmann@36712:     "\<not> P \<Longrightarrow> (P \<equiv> False)"
haftmann@36712:   by auto
haftmann@36712: 
haftmann@36712: ML {*
wenzelm@45294: structure Algebra_Simplification = Named_Thms
wenzelm@45294: (
wenzelm@45294:   val name = @{binding algebra}
haftmann@36712:   val description = "pre-simplification rules for algebraic methods"
haftmann@36712: )
haftmann@28402: *}
haftmann@28402: 
haftmann@36712: setup Algebra_Simplification.setup
haftmann@36712: 
wenzelm@48891: ML_file "Tools/groebner.ML"
haftmann@36751: 
wenzelm@47432: method_setup algebra = {*
wenzelm@47432:   let
wenzelm@47432:     fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
wenzelm@47432:     val addN = "add"
wenzelm@47432:     val delN = "del"
wenzelm@47432:     val any_keyword = keyword addN || keyword delN
wenzelm@47432:     val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
wenzelm@47432:   in
wenzelm@47432:     Scan.optional (keyword addN |-- thms) [] --
wenzelm@47432:      Scan.optional (keyword delN |-- thms) [] >>
wenzelm@47432:     (fn (add_ths, del_ths) => fn ctxt =>
wenzelm@47432:       SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
wenzelm@47432:   end
wenzelm@47432: *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
haftmann@36751: 
haftmann@36712: declare dvd_def[algebra]
haftmann@36712: declare dvd_eq_mod_eq_0[symmetric, algebra]
haftmann@36712: declare mod_div_trivial[algebra]
haftmann@36712: declare mod_mod_trivial[algebra]
huffman@47142: declare div_by_0[algebra]
huffman@47142: declare mod_by_0[algebra]
haftmann@36712: declare zmod_zdiv_equality[symmetric,algebra]
huffman@47165: declare div_mod_equality2[symmetric, algebra]
huffman@47159: declare div_minus_minus[algebra]
huffman@47159: declare mod_minus_minus[algebra]
huffman@47159: declare div_minus_right[algebra]
huffman@47159: declare mod_minus_right[algebra]
huffman@47142: declare div_0[algebra]
huffman@47142: declare mod_0[algebra]
haftmann@36712: declare mod_by_1[algebra]
haftmann@36712: declare div_by_1[algebra]
huffman@47160: declare mod_minus1_right[algebra]
huffman@47160: declare div_minus1_right[algebra]
haftmann@36712: declare mod_mult_self2_is_0[algebra]
haftmann@36712: declare mod_mult_self1_is_0[algebra]
haftmann@36712: declare zmod_eq_0_iff[algebra]
haftmann@36712: declare dvd_0_left_iff[algebra]
haftmann@36712: declare zdvd1_eq[algebra]
haftmann@36712: declare zmod_eq_dvd_iff[algebra]
haftmann@36712: declare nat_mod_eq_iff[algebra]
haftmann@36712: 
haftmann@28402: end