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