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