src/HOL/Groebner_Basis.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (23 months ago)
changeset 66831 29ea2b900a05
parent 64593 50c715579715
child 67091 1393c2340eec
permissions -rw-r--r--
tuned: each session has at most one defining entry;
wenzelm@23252
     1
(*  Title:      HOL/Groebner_Basis.thy
wenzelm@23252
     2
    Author:     Amine Chaieb, TU Muenchen
wenzelm@23252
     3
*)
wenzelm@23252
     4
wenzelm@60758
     5
section \<open>Groebner bases\<close>
haftmann@28402
     6
wenzelm@23252
     7
theory Groebner_Basis
haftmann@58777
     8
imports Semiring_Normalization Parity
wenzelm@23252
     9
begin
wenzelm@23252
    10
wenzelm@60758
    11
subsection \<open>Groebner Bases\<close>
haftmann@36712
    12
wenzelm@61799
    13
lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to @{theory HOL}\<close>
haftmann@54251
    14
wenzelm@61799
    15
lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in @{theory HOL}\<close>
haftmann@54251
    16
  "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
haftmann@54251
    17
  "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
haftmann@54251
    18
  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
haftmann@54251
    19
  by blast+
haftmann@36712
    20
haftmann@36712
    21
lemma dnf:
haftmann@54251
    22
  "(P & (Q | R)) = ((P&Q) | (P&R))"
haftmann@54251
    23
  "((Q | R) & P) = ((Q&P) | (R&P))"
haftmann@54251
    24
  "(P \<and> Q) = (Q \<and> P)"
haftmann@54251
    25
  "(P \<or> Q) = (Q \<or> P)"
haftmann@36712
    26
  by blast+
haftmann@36712
    27
haftmann@36712
    28
lemmas weak_dnf_simps = dnf bool_simps
haftmann@36712
    29
haftmann@36712
    30
lemma PFalse:
haftmann@36712
    31
    "P \<equiv> False \<Longrightarrow> \<not> P"
haftmann@36712
    32
    "\<not> P \<Longrightarrow> (P \<equiv> False)"
haftmann@36712
    33
  by auto
haftmann@36712
    34
wenzelm@57951
    35
named_theorems algebra "pre-simplification rules for algebraic methods"
wenzelm@48891
    36
ML_file "Tools/groebner.ML"
haftmann@36751
    37
wenzelm@60758
    38
method_setup algebra = \<open>
wenzelm@47432
    39
  let
wenzelm@47432
    40
    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
wenzelm@47432
    41
    val addN = "add"
wenzelm@47432
    42
    val delN = "del"
wenzelm@47432
    43
    val any_keyword = keyword addN || keyword delN
wenzelm@61476
    44
    val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
wenzelm@47432
    45
  in
wenzelm@47432
    46
    Scan.optional (keyword addN |-- thms) [] --
wenzelm@47432
    47
     Scan.optional (keyword delN |-- thms) [] >>
wenzelm@47432
    48
    (fn (add_ths, del_ths) => fn ctxt =>
wenzelm@47432
    49
      SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
wenzelm@47432
    50
  end
wenzelm@60758
    51
\<close> "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
haftmann@36751
    52
haftmann@36712
    53
declare dvd_def[algebra]
haftmann@64248
    54
declare mod_eq_0_iff_dvd[algebra]
haftmann@36712
    55
declare mod_div_trivial[algebra]
haftmann@36712
    56
declare mod_mod_trivial[algebra]
huffman@47142
    57
declare div_by_0[algebra]
huffman@47142
    58
declare mod_by_0[algebra]
haftmann@64246
    59
declare mult_div_mod_eq[algebra]
huffman@47159
    60
declare div_minus_minus[algebra]
huffman@47159
    61
declare mod_minus_minus[algebra]
huffman@47159
    62
declare div_minus_right[algebra]
huffman@47159
    63
declare mod_minus_right[algebra]
huffman@47142
    64
declare div_0[algebra]
huffman@47142
    65
declare mod_0[algebra]
haftmann@36712
    66
declare mod_by_1[algebra]
haftmann@36712
    67
declare div_by_1[algebra]
huffman@47160
    68
declare mod_minus1_right[algebra]
huffman@47160
    69
declare div_minus1_right[algebra]
haftmann@36712
    70
declare mod_mult_self2_is_0[algebra]
haftmann@36712
    71
declare mod_mult_self1_is_0[algebra]
haftmann@36712
    72
declare zmod_eq_0_iff[algebra]
haftmann@36712
    73
declare dvd_0_left_iff[algebra]
haftmann@36712
    74
declare zdvd1_eq[algebra]
haftmann@64593
    75
declare mod_eq_dvd_iff[algebra]
haftmann@36712
    76
declare nat_mod_eq_iff[algebra]
haftmann@36712
    77
haftmann@58777
    78
context semiring_parity
haftmann@58777
    79
begin
haftmann@58777
    80
haftmann@58777
    81
declare even_times_iff [algebra]
haftmann@58777
    82
declare even_power [algebra]
haftmann@58777
    83
haftmann@28402
    84
end
haftmann@58777
    85
haftmann@58777
    86
context ring_parity
haftmann@58777
    87
begin
haftmann@58777
    88
haftmann@58777
    89
declare even_minus [algebra]
haftmann@58777
    90
haftmann@58777
    91
end
haftmann@58777
    92
haftmann@58777
    93
declare even_Suc [algebra]
haftmann@58777
    94
declare even_diff_nat [algebra]
haftmann@58777
    95
haftmann@58777
    96
end