src/HOL/Groebner_Basis.thy
 author haftmann Fri May 07 15:05:52 2010 +0200 (2010-05-07) changeset 36751 7f1da69cacb3 parent 36720 41da7025e59c child 36752 cf558aeb35b0 permissions -rw-r--r--
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
```     1 (*  Title:      HOL/Groebner_Basis.thy
```
```     2     Author:     Amine Chaieb, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 header {* Groebner bases *}
```
```     6
```
```     7 theory Groebner_Basis
```
```     8 imports Semiring_Normalization
```
```     9 uses
```
```    10   ("Tools/Groebner_Basis/groebner.ML")
```
```    11 begin
```
```    12
```
```    13 subsection {* Groebner Bases *}
```
```    14
```
```    15 lemmas bool_simps = simp_thms(1-34)
```
```    16
```
```    17 lemma dnf:
```
```    18     "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
```
```    19     "(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"
```
```    20   by blast+
```
```    21
```
```    22 lemmas weak_dnf_simps = dnf bool_simps
```
```    23
```
```    24 lemma nnf_simps:
```
```    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)"
```
```    26     "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
```
```    27   by blast+
```
```    28
```
```    29 lemma PFalse:
```
```    30     "P \<equiv> False \<Longrightarrow> \<not> P"
```
```    31     "\<not> P \<Longrightarrow> (P \<equiv> False)"
```
```    32   by auto
```
```    33
```
```    34 ML {*
```
```    35 structure Algebra_Simplification = Named_Thms(
```
```    36   val name = "algebra"
```
```    37   val description = "pre-simplification rules for algebraic methods"
```
```    38 )
```
```    39 *}
```
```    40
```
```    41 setup Algebra_Simplification.setup
```
```    42
```
```    43 use "Tools/Groebner_Basis/groebner.ML"
```
```    44
```
```    45 method_setup algebra = Groebner.algebra_method
```
```    46   "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
```
```    47
```
```    48 declare dvd_def[algebra]
```
```    49 declare dvd_eq_mod_eq_0[symmetric, algebra]
```
```    50 declare mod_div_trivial[algebra]
```
```    51 declare mod_mod_trivial[algebra]
```
```    52 declare conjunct1[OF DIVISION_BY_ZERO, algebra]
```
```    53 declare conjunct2[OF DIVISION_BY_ZERO, algebra]
```
```    54 declare zmod_zdiv_equality[symmetric,algebra]
```
```    55 declare zdiv_zmod_equality[symmetric, algebra]
```
```    56 declare zdiv_zminus_zminus[algebra]
```
```    57 declare zmod_zminus_zminus[algebra]
```
```    58 declare zdiv_zminus2[algebra]
```
```    59 declare zmod_zminus2[algebra]
```
```    60 declare zdiv_zero[algebra]
```
```    61 declare zmod_zero[algebra]
```
```    62 declare mod_by_1[algebra]
```
```    63 declare div_by_1[algebra]
```
```    64 declare zmod_minus1_right[algebra]
```
```    65 declare zdiv_minus1_right[algebra]
```
```    66 declare mod_div_trivial[algebra]
```
```    67 declare mod_mod_trivial[algebra]
```
```    68 declare mod_mult_self2_is_0[algebra]
```
```    69 declare mod_mult_self1_is_0[algebra]
```
```    70 declare zmod_eq_0_iff[algebra]
```
```    71 declare dvd_0_left_iff[algebra]
```
```    72 declare zdvd1_eq[algebra]
```
```    73 declare zmod_eq_dvd_iff[algebra]
```
```    74 declare nat_mod_eq_iff[algebra]
```
```    75
```
```    76 end
```