(* Title: HOL/Groebner_Basis.thy
Author: Amine Chaieb, TU Muenchen
*)
section \<open>Groebner bases\<close>
theory Groebner_Basis
imports Semiring_Normalization Parity
begin
subsection \<open>Groebner Bases\<close>
lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to \<^theory>\<open>HOL.HOL\<close>\<close>
lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in \<^theory>\<open>HOL.HOL\<close>\<close>
"(\(P \ Q)) = (\P \ \Q)" "(\(P \ Q)) = (\P \ \Q)"
"(P \ Q) = (\P \ Q)"
"(P = Q) = ((P \ Q) \ (\P \ \ Q))" "(\ \(P)) = P"
by blast+
lemma dnf:
"(P \ (Q \ R)) = ((P\Q) \ (P\R))"
"((Q \ R) \ P) = ((Q\P) \ (R\P))"
"(P \ Q) = (Q \ P)"
"(P \ Q) = (Q \ P)"
by blast+
lemmas weak_dnf_simps = dnf bool_simps
lemma PFalse:
"P \ False \ \ P"
"\ P \ (P \ False)"
by auto
named_theorems algebra "pre-simplification rules for algebraic methods"
ML_file \<open>Tools/groebner.ML\<close>
method_setup algebra = \<open>
let
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
val addN = "add"
val delN = "del"
val any_keyword = keyword addN || keyword delN
val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
in
Scan.optional (keyword addN |-- thms) [] --
Scan.optional (keyword delN |-- thms) [] >>
(fn (add_ths, del_ths) => fn ctxt =>
SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
end
\<close> "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
declare dvd_def[algebra]
declare mod_eq_0_iff_dvd[algebra]
declare mod_div_trivial[algebra]
declare mod_mod_trivial[algebra]
declare div_by_0[algebra]
declare mod_by_0[algebra]
declare mult_div_mod_eq[algebra]
declare div_minus_minus[algebra]
declare mod_minus_minus[algebra]
declare div_minus_right[algebra]
declare mod_minus_right[algebra]
declare div_0[algebra]
declare mod_0[algebra]
declare mod_by_1[algebra]
declare div_by_1[algebra]
declare mod_minus1_right[algebra]
declare div_minus1_right[algebra]
declare mod_mult_self2_is_0[algebra]
declare mod_mult_self1_is_0[algebra]
declare zmod_eq_0_iff[algebra]
declare dvd_0_left_iff[algebra]
declare zdvd1_eq[algebra]
declare mod_eq_dvd_iff[algebra]
declare nat_mod_eq_iff[algebra]
context semiring_parity
begin
declare even_mult_iff [algebra]
declare even_power [algebra]
end
context ring_parity
begin
declare even_minus [algebra]
end
declare even_Suc [algebra]
declare even_diff_nat [algebra]
end
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
