author  haftmann 
Fri, 07 May 2010 15:05:52 +0200  
changeset 36751  7f1da69cacb3 
parent 36720  41da7025e59c 
child 36752  cf558aeb35b0 
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 
23312  10 
("Tools/Groebner_Basis/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 {* 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

35 
structure Algebra_Simplification = Named_Thms( 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

36 
val name = "algebra" 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

37 
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

38 
) 
28402  39 
*} 
40 

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

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

42 

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

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

44 

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

45 
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

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

47 

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

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

49 
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

50 
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

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

52 
declare conjunct1[OF DIVISION_BY_ZERO, algebra] 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

53 
declare conjunct2[OF DIVISION_BY_ZERO, algebra] 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

54 
declare zmod_zdiv_equality[symmetric,algebra] 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

55 
declare zdiv_zmod_equality[symmetric, algebra] 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

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

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

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

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

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

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

62 
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

63 
declare div_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 zmod_minus1_right[algebra] 
2f4c318861b3
avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents:
36702
diff
changeset

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

66 
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

67 
declare mod_mod_trivial[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_self2_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 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

70 
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

71 
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

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

73 
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

74 
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

75 

28402  76 
end 