src/HOL/Groebner_Basis.thy
author webertj
Fri, 19 Oct 2012 15:12:52 +0200
changeset 49962 a8cc904a6820
parent 48891 c0eafbd55de3
child 54251 adea9f6986b2
permissions -rw-r--r--
Renamed {left,right}_distrib to distrib_{right,left}.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23252
67268bb40b21 Semiring normalization and Groebner Bases.
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Groebner_Basis.thy
67268bb40b21 Semiring normalization and Groebner Bases.
wenzelm
parents:
diff changeset
     2
    Author:     Amine Chaieb, TU Muenchen
67268bb40b21 Semiring normalization and Groebner Bases.
wenzelm
parents:
diff changeset
     3
*)
67268bb40b21 Semiring normalization and Groebner Bases.
wenzelm
parents:
diff changeset
     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
09e4aa3ddc25 clarified dependencies between arith tools
haftmann
parents: 27666
diff changeset
     6
23252
67268bb40b21 Semiring normalization and Groebner Bases.
wenzelm
parents:
diff changeset
     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
67268bb40b21 Semiring normalization and Groebner Bases.
wenzelm
parents:
diff changeset
     9
begin
67268bb40b21 Semiring normalization and Groebner Bases.
wenzelm
parents:
diff changeset
    10
36712
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    11
subsection {* Groebner Bases *}
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    12
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    13
lemmas bool_simps = simp_thms(1-34)
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
lemma dnf:
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    16
    "(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
    17
    "(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
    18
  by blast+
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    19
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    20
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
    21
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    22
lemma nnf_simps:
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    23
    "(\<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
    24
    "(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
    25
  by blast+
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    26
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    27
lemma PFalse:
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    28
    "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
    29
    "\<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
    30
  by auto
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    31
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    32
ML {*
45294
3c5d3d286055 tuned Named_Thms: proper binding;
wenzelm
parents: 36752
diff changeset
    33
structure Algebra_Simplification = Named_Thms
3c5d3d286055 tuned Named_Thms: proper binding;
wenzelm
parents: 36752
diff changeset
    34
(
3c5d3d286055 tuned Named_Thms: proper binding;
wenzelm
parents: 36752
diff changeset
    35
  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
    36
  val description = "pre-simplification rules for algebraic methods"
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    37
)
28402
09e4aa3ddc25 clarified dependencies between arith tools
haftmann
parents: 27666
diff changeset
    38
*}
09e4aa3ddc25 clarified dependencies between arith tools
haftmann
parents: 27666
diff changeset
    39
36712
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    40
setup Algebra_Simplification.setup
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    41
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47432
diff changeset
    42
ML_file "Tools/groebner.ML"
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36720
diff changeset
    43
47432
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    44
method_setup algebra = {*
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    45
  let
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    46
    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    47
    val addN = "add"
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    48
    val delN = "del"
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    49
    val any_keyword = keyword addN || keyword delN
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    50
    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    51
  in
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    52
    Scan.optional (keyword addN |-- thms) [] --
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    53
     Scan.optional (keyword delN |-- thms) [] >>
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    54
    (fn (add_ths, del_ths) => fn ctxt =>
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    55
      SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    56
  end
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    57
*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36720
diff changeset
    58
36712
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    59
declare dvd_def[algebra]
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    60
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
    61
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
    62
declare mod_mod_trivial[algebra]
47142
d64fa2ca54b8 remove redundant lemmas
huffman
parents: 45294
diff changeset
    63
declare div_by_0[algebra]
d64fa2ca54b8 remove redundant lemmas
huffman
parents: 45294
diff changeset
    64
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
    65
declare zmod_zdiv_equality[symmetric,algebra]
47165
9344891b504b remove redundant lemmas
huffman
parents: 47161
diff changeset
    66
declare div_mod_equality2[symmetric, algebra]
47159
978c00c20a59 generalize some theorems about div/mod
huffman
parents: 47142
diff changeset
    67
declare div_minus_minus[algebra]
978c00c20a59 generalize some theorems about div/mod
huffman
parents: 47142
diff changeset
    68
declare mod_minus_minus[algebra]
978c00c20a59 generalize some theorems about div/mod
huffman
parents: 47142
diff changeset
    69
declare div_minus_right[algebra]
978c00c20a59 generalize some theorems about div/mod
huffman
parents: 47142
diff changeset
    70
declare mod_minus_right[algebra]
47142
d64fa2ca54b8 remove redundant lemmas
huffman
parents: 45294
diff changeset
    71
declare div_0[algebra]
d64fa2ca54b8 remove redundant lemmas
huffman
parents: 45294
diff changeset
    72
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
    73
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
    74
declare div_by_1[algebra]
47160
8ada79014cb2 generalize more div/mod lemmas
huffman
parents: 47159
diff changeset
    75
declare mod_minus1_right[algebra]
8ada79014cb2 generalize more div/mod lemmas
huffman
parents: 47159
diff changeset
    76
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
    77
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
    78
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
    79
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
    80
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
    81
declare zdvd1_eq[algebra]
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    82
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
    83
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
    84
28402
09e4aa3ddc25 clarified dependencies between arith tools
haftmann
parents: 27666
diff changeset
    85
end