author | wenzelm |
Sun, 02 Nov 2014 18:21:45 +0100 | |
changeset 58889 | 5b7a9633cfa8 |
parent 58777 | 6ba2f1fa243b |
child 58925 | 1b655309617c |
permissions | -rw-r--r-- |
23252 | 1 |
(* Title: HOL/Groebner_Basis.thy |
2 |
Author: Amine Chaieb, TU Muenchen |
|
3 |
*) |
|
4 |
||
58889 | 5 |
section {* Groebner bases *} |
28402 | 6 |
|
23252 | 7 |
theory Groebner_Basis |
58777
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
8 |
imports Semiring_Normalization Parity |
55509
bd67ebe275e0
eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817)
haftmann
parents:
55178
diff
changeset
|
9 |
keywords "try0" :: diag |
23252 | 10 |
begin |
11 |
||
36712
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
12 |
subsection {* Groebner Bases *} |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
13 |
|
54251 | 14 |
lemmas bool_simps = simp_thms(1-34) -- {* FIXME move to @{theory HOL} *} |
15 |
||
16 |
lemma nnf_simps: -- {* FIXME shadows fact binding in @{theory HOL} *} |
|
17 |
"(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" |
|
18 |
"(P \<longrightarrow> Q) = (\<not>P \<or> Q)" |
|
19 |
"(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P" |
|
20 |
by blast+ |
|
36712
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
21 |
|
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
22 |
lemma dnf: |
54251 | 23 |
"(P & (Q | R)) = ((P&Q) | (P&R))" |
24 |
"((Q | R) & P) = ((Q&P) | (R&P))" |
|
25 |
"(P \<and> Q) = (Q \<and> P)" |
|
26 |
"(P \<or> Q) = (Q \<or> P)" |
|
36712
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
27 |
by blast+ |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
28 |
|
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
29 |
lemmas weak_dnf_simps = dnf bool_simps |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
30 |
|
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
31 |
lemma PFalse: |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
32 |
"P \<equiv> False \<Longrightarrow> \<not> P" |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
33 |
"\<not> P \<Longrightarrow> (P \<equiv> False)" |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
34 |
by auto |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
35 |
|
57951 | 36 |
named_theorems algebra "pre-simplification rules for algebraic methods" |
48891 | 37 |
ML_file "Tools/groebner.ML" |
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36720
diff
changeset
|
38 |
|
47432 | 39 |
method_setup algebra = {* |
40 |
let |
|
41 |
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () |
|
42 |
val addN = "add" |
|
43 |
val delN = "del" |
|
44 |
val any_keyword = keyword addN || keyword delN |
|
45 |
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
|
46 |
in |
|
47 |
Scan.optional (keyword addN |-- thms) [] -- |
|
48 |
Scan.optional (keyword delN |-- thms) [] >> |
|
49 |
(fn (add_ths, del_ths) => fn ctxt => |
|
50 |
SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt)) |
|
51 |
end |
|
52 |
*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" |
|
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36720
diff
changeset
|
53 |
|
36712
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
54 |
declare dvd_def[algebra] |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
55 |
declare dvd_eq_mod_eq_0[symmetric, algebra] |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
56 |
declare mod_div_trivial[algebra] |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
57 |
declare mod_mod_trivial[algebra] |
47142 | 58 |
declare div_by_0[algebra] |
59 |
declare mod_by_0[algebra] |
|
36712
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
60 |
declare zmod_zdiv_equality[symmetric,algebra] |
47165 | 61 |
declare div_mod_equality2[symmetric, algebra] |
47159 | 62 |
declare div_minus_minus[algebra] |
63 |
declare mod_minus_minus[algebra] |
|
64 |
declare div_minus_right[algebra] |
|
65 |
declare mod_minus_right[algebra] |
|
47142 | 66 |
declare div_0[algebra] |
67 |
declare mod_0[algebra] |
|
36712
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
68 |
declare mod_by_1[algebra] |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
69 |
declare div_by_1[algebra] |
47160 | 70 |
declare mod_minus1_right[algebra] |
71 |
declare div_minus1_right[algebra] |
|
36712
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
72 |
declare mod_mult_self2_is_0[algebra] |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
73 |
declare mod_mult_self1_is_0[algebra] |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
74 |
declare zmod_eq_0_iff[algebra] |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
75 |
declare dvd_0_left_iff[algebra] |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
76 |
declare zdvd1_eq[algebra] |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
77 |
declare zmod_eq_dvd_iff[algebra] |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
78 |
declare nat_mod_eq_iff[algebra] |
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset
|
79 |
|
58777
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
80 |
context semiring_parity |
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
81 |
begin |
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
82 |
|
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
83 |
declare even_times_iff [algebra] |
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
84 |
declare even_power [algebra] |
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
85 |
|
28402 | 86 |
end |
58777
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
87 |
|
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
88 |
context ring_parity |
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
89 |
begin |
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
90 |
|
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
91 |
declare even_minus [algebra] |
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
92 |
|
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
93 |
end |
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
94 |
|
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
95 |
declare even_Suc [algebra] |
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
96 |
declare even_diff_nat [algebra] |
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
97 |
|
6ba2f1fa243b
further downshift of theory Parity in the hierarchy
haftmann
parents:
57951
diff
changeset
|
98 |
end |