author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47165  9344891b504b 
child 47432  e1576d13e933 
permissions  rwrr 
23252  1 
(* Title: HOL/Groebner_Basis.thy 
2 
Author: Amine Chaieb, TU Muenchen 

3 
*) 

4 

36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36720
diff
changeset

5 
header {* Groebner bases *} 
28402  6 

23252  7 
theory Groebner_Basis 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36720
diff
changeset

8 
imports Semiring_Normalization 
23252  9 
uses 
36752
cf558aeb35b0
delete Groebner_Basis directory  only one file left
haftmann
parents:
36751
diff
changeset

10 
("Tools/groebner.ML") 
23252  11 
begin 
12 

36712
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

13 
subsection {* Groebner Bases *} 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

14 

2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

15 
lemmas bool_simps = simp_thms(134) 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

16 

2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

17 
lemma dnf: 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

18 
"(P & (Q  R)) = ((P&Q)  (P&R))" "((Q  R) & P) = ((Q&P)  (R&P))" 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

19 
"(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)" 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

20 
by blast+ 
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 
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

23 

2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

24 
lemma nnf_simps: 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

25 
"(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)" 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

26 
"(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P" 
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 
lemma PFalse: 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

30 
"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

31 
"\<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

32 
by auto 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

33 

2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

34 
ML {* 
45294  35 
structure Algebra_Simplification = Named_Thms 
36 
( 

37 
val name = @{binding algebra} 

36712
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

38 
val description = "presimplification rules for algebraic methods" 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

39 
) 
28402  40 
*} 
41 

36712
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

42 
setup Algebra_Simplification.setup 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

43 

36752
cf558aeb35b0
delete Groebner_Basis directory  only one file left
haftmann
parents:
36751
diff
changeset

44 
use "Tools/groebner.ML" 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36720
diff
changeset

45 

7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36720
diff
changeset

46 
method_setup algebra = Groebner.algebra_method 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36720
diff
changeset

47 
"solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36720
diff
changeset

48 

36712
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

49 
declare dvd_def[algebra] 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

50 
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

51 
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

52 
declare mod_mod_trivial[algebra] 
47142  53 
declare div_by_0[algebra] 
54 
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

55 
declare zmod_zdiv_equality[symmetric,algebra] 
47165  56 
declare div_mod_equality2[symmetric, algebra] 
47159  57 
declare div_minus_minus[algebra] 
58 
declare mod_minus_minus[algebra] 

59 
declare div_minus_right[algebra] 

60 
declare mod_minus_right[algebra] 

47142  61 
declare div_0[algebra] 
62 
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

63 
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

64 
declare div_by_1[algebra] 
47160  65 
declare mod_minus1_right[algebra] 
66 
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

67 
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

68 
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

69 
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

70 
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

71 
declare zdvd1_eq[algebra] 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

72 
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

73 
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

74 

28402  75 
end 