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