(* Title: HOL/Groebner_Basis.thy Author: Amine Chaieb, TU Muenchen *) header {* Groebner bases *} theory Groebner_Basis imports Semiring_Normalization begin subsection {* Groebner Bases *} lemmas bool_simps = simp_thms(1-34) 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 nnf_simps: "(\(P \ Q)) = (\P \ \Q)" "(\(P \ Q)) = (\P \ \Q)" "(P \ Q) = (\P \ Q)" "(P = Q) = ((P \ Q) \ (\P \ \ Q))" "(\ \(P)) = P" by blast+ lemma PFalse: "P \ False \ \ P" "\ P \ (P \ False)" by auto ML {* structure Algebra_Simplification = Named_Thms ( val name = @{binding algebra} val description = "pre-simplification rules for algebraic methods" ) *} setup Algebra_Simplification.setup ML_file "Tools/groebner.ML" method_setup algebra = {* 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.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; 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 *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" declare dvd_def[algebra] declare dvd_eq_mod_eq_0[symmetric, algebra] declare mod_div_trivial[algebra] declare mod_mod_trivial[algebra] declare div_by_0[algebra] declare mod_by_0[algebra] declare zmod_zdiv_equality[symmetric,algebra] declare div_mod_equality2[symmetric, 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 zmod_eq_dvd_iff[algebra] declare nat_mod_eq_iff[algebra] end