src/HOL/Groebner_Basis.thy
author paulson <lp15@cam.ac.uk>
Tue, 30 May 2023 12:33:06 +0100
changeset 78127 24b70433c2e8
parent 76224 64e8d4afcf10
permissions -rw-r--r--
New HOL Light material on metric spaces and topological spaces
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
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58925
diff changeset
     5
section \<open>Groebner bases\<close>
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
58777
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
     8
imports Semiring_Normalization Parity
23252
67268bb40b21 Semiring normalization and Groebner Bases.
wenzelm
parents:
diff changeset
     9
begin
67268bb40b21 Semiring normalization and Groebner Bases.
wenzelm
parents:
diff changeset
    10
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58925
diff changeset
    11
subsection \<open>Groebner Bases\<close>
36712
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    12
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 68484
diff changeset
    13
lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to \<^theory>\<open>HOL.HOL\<close>\<close>
54251
adea9f6986b2 dropped dead code
haftmann
parents: 48891
diff changeset
    14
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 68484
diff changeset
    15
lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in \<^theory>\<open>HOL.HOL\<close>\<close>
54251
adea9f6986b2 dropped dead code
haftmann
parents: 48891
diff changeset
    16
  "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
adea9f6986b2 dropped dead code
haftmann
parents: 48891
diff changeset
    17
  "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
adea9f6986b2 dropped dead code
haftmann
parents: 48891
diff changeset
    18
  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
adea9f6986b2 dropped dead code
haftmann
parents: 48891
diff changeset
    19
  by blast+
36712
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    20
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    21
lemma dnf:
67091
1393c2340eec more symbols;
wenzelm
parents: 64593
diff changeset
    22
  "(P \<and> (Q \<or> R)) = ((P\<and>Q) \<or> (P\<and>R))"
1393c2340eec more symbols;
wenzelm
parents: 64593
diff changeset
    23
  "((Q \<or> R) \<and> P) = ((Q\<and>P) \<or> (R\<and>P))"
54251
adea9f6986b2 dropped dead code
haftmann
parents: 48891
diff changeset
    24
  "(P \<and> Q) = (Q \<and> P)"
adea9f6986b2 dropped dead code
haftmann
parents: 48891
diff changeset
    25
  "(P \<or> Q) = (Q \<or> P)"
36712
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    26
  by blast+
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    27
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    28
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
    29
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    30
lemma PFalse:
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    31
    "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
    32
    "\<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
    33
  by auto
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    34
57951
7896762b638b updated to named_theorems;
wenzelm
parents: 56850
diff changeset
    35
named_theorems algebra "pre-simplification rules for algebraic methods"
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    36
ML_file \<open>Tools/groebner.ML\<close>
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36720
diff changeset
    37
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58925
diff changeset
    38
method_setup algebra = \<open>
47432
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    39
  let
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    40
    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    41
    val addN = "add"
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    42
    val delN = "del"
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    43
    val any_keyword = keyword addN || keyword delN
61476
1884c40f1539 tuned signature;
wenzelm
parents: 60758
diff changeset
    44
    val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
47432
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    45
  in
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    46
    Scan.optional (keyword addN |-- thms) [] --
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    47
     Scan.optional (keyword delN |-- thms) [] >>
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    48
    (fn (add_ths, del_ths) => fn ctxt =>
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    49
      SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
e1576d13e933 more standard method setup;
wenzelm
parents: 47165
diff changeset
    50
  end
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58925
diff changeset
    51
\<close> "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
    52
36712
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    53
declare dvd_def[algebra]
64248
690eb1ae8bb0 simplified fact references
haftmann
parents: 64246
diff changeset
    54
declare mod_eq_0_iff_dvd[algebra]
36712
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    55
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
    56
declare mod_mod_trivial[algebra]
47142
d64fa2ca54b8 remove redundant lemmas
huffman
parents: 45294
diff changeset
    57
declare div_by_0[algebra]
d64fa2ca54b8 remove redundant lemmas
huffman
parents: 45294
diff changeset
    58
declare mod_by_0[algebra]
64246
15d1ee6e847b eliminated irregular aliasses
haftmann
parents: 61799
diff changeset
    59
declare mult_div_mod_eq[algebra]
47159
978c00c20a59 generalize some theorems about div/mod
huffman
parents: 47142
diff changeset
    60
declare div_minus_minus[algebra]
978c00c20a59 generalize some theorems about div/mod
huffman
parents: 47142
diff changeset
    61
declare mod_minus_minus[algebra]
978c00c20a59 generalize some theorems about div/mod
huffman
parents: 47142
diff changeset
    62
declare div_minus_right[algebra]
978c00c20a59 generalize some theorems about div/mod
huffman
parents: 47142
diff changeset
    63
declare mod_minus_right[algebra]
47142
d64fa2ca54b8 remove redundant lemmas
huffman
parents: 45294
diff changeset
    64
declare div_0[algebra]
d64fa2ca54b8 remove redundant lemmas
huffman
parents: 45294
diff changeset
    65
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
    66
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
    67
declare div_by_1[algebra]
47160
8ada79014cb2 generalize more div/mod lemmas
huffman
parents: 47159
diff changeset
    68
declare mod_minus1_right[algebra]
8ada79014cb2 generalize more div/mod lemmas
huffman
parents: 47159
diff changeset
    69
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
    70
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
    71
declare mod_mult_self1_is_0[algebra]
76224
64e8d4afcf10 moved relevant theorems from theory Divides to theory Euclidean_Division
haftmann
parents: 70341
diff changeset
    72
64e8d4afcf10 moved relevant theorems from theory Divides to theory Euclidean_Division
haftmann
parents: 70341
diff changeset
    73
lemma zmod_eq_0_iff [algebra]:
64e8d4afcf10 moved relevant theorems from theory Divides to theory Euclidean_Division
haftmann
parents: 70341
diff changeset
    74
  \<open>m mod d = 0 \<longleftrightarrow> (\<exists>q. m = d * q)\<close> for m d :: int
64e8d4afcf10 moved relevant theorems from theory Divides to theory Euclidean_Division
haftmann
parents: 70341
diff changeset
    75
  by (auto simp add: mod_eq_0_iff_dvd)
64e8d4afcf10 moved relevant theorems from theory Divides to theory Euclidean_Division
haftmann
parents: 70341
diff changeset
    76
36712
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    77
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
    78
declare zdvd1_eq[algebra]
64593
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 64249
diff changeset
    79
declare mod_eq_dvd_iff[algebra]
36712
2f4c318861b3 avoid references to groebner bases in names which have no references to groebner bases
haftmann
parents: 36702
diff changeset
    80
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
    81
70341
972c0c744e7c generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents: 70340
diff changeset
    82
context semiring_parity
58777
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    83
begin
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    84
68100
b2d84b1114fa removed some lemma duplicates
haftmann
parents: 67091
diff changeset
    85
declare even_mult_iff [algebra]
58777
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    86
declare even_power [algebra]
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    87
28402
09e4aa3ddc25 clarified dependencies between arith tools
haftmann
parents: 27666
diff changeset
    88
end
58777
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    89
70341
972c0c744e7c generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents: 70340
diff changeset
    90
context ring_parity
58777
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    91
begin
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    92
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    93
declare even_minus [algebra]
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    94
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    95
end
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    96
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    97
declare even_Suc [algebra]
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    98
declare even_diff_nat [algebra]
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
    99
6ba2f1fa243b further downshift of theory Parity in the hierarchy
haftmann
parents: 57951
diff changeset
   100
end