src/HOL/Groebner_Basis.thy
author huffman
Tue Mar 27 14:49:56 2012 +0200 (2012-03-27)
changeset 47142 d64fa2ca54b8
parent 45294 3c5d3d286055
child 47159 978c00c20a59
permissions -rw-r--r--
remove redundant lemmas
     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.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 (
    37   val name = @{binding algebra}
    38   val description = "pre-simplification rules for algebraic methods"
    39 )
    40 *}
    41 
    42 setup Algebra_Simplification.setup
    43 
    44 use "Tools/groebner.ML"
    45 
    46 method_setup algebra = Groebner.algebra_method
    47   "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
    48 
    49 declare dvd_def[algebra]
    50 declare dvd_eq_mod_eq_0[symmetric, algebra]
    51 declare mod_div_trivial[algebra]
    52 declare mod_mod_trivial[algebra]
    53 declare div_by_0[algebra]
    54 declare mod_by_0[algebra]
    55 declare zmod_zdiv_equality[symmetric,algebra]
    56 declare zdiv_zmod_equality[symmetric, algebra]
    57 declare zdiv_zminus_zminus[algebra]
    58 declare zmod_zminus_zminus[algebra]
    59 declare zdiv_zminus2[algebra]
    60 declare zmod_zminus2[algebra]
    61 declare div_0[algebra]
    62 declare mod_0[algebra]
    63 declare mod_by_1[algebra]
    64 declare div_by_1[algebra]
    65 declare zmod_minus1_right[algebra]
    66 declare zdiv_minus1_right[algebra]
    67 declare mod_div_trivial[algebra]
    68 declare mod_mod_trivial[algebra]
    69 declare mod_mult_self2_is_0[algebra]
    70 declare mod_mult_self1_is_0[algebra]
    71 declare zmod_eq_0_iff[algebra]
    72 declare dvd_0_left_iff[algebra]
    73 declare zdvd1_eq[algebra]
    74 declare zmod_eq_dvd_iff[algebra]
    75 declare nat_mod_eq_iff[algebra]
    76 
    77 end