src/HOL/Groebner_Basis.thy
author blanchet
Sun May 04 18:53:58 2014 +0200 (2014-05-04)
changeset 56850 13a7bca533a3
parent 55509 bd67ebe275e0
child 57951 7896762b638b
permissions -rw-r--r--
added 'satx' proof method to Try0
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
haftmann@55509
     9
keywords "try0" :: diag
wenzelm@23252
    10
begin
wenzelm@23252
    11
haftmann@36712
    12
subsection {* Groebner Bases *}
haftmann@36712
    13
haftmann@54251
    14
lemmas bool_simps = simp_thms(1-34) -- {* FIXME move to @{theory HOL} *}
haftmann@54251
    15
haftmann@54251
    16
lemma nnf_simps: -- {* FIXME shadows fact binding in @{theory HOL} *}
haftmann@54251
    17
  "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
haftmann@54251
    18
  "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
haftmann@54251
    19
  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
haftmann@54251
    20
  by blast+
haftmann@36712
    21
haftmann@36712
    22
lemma dnf:
haftmann@54251
    23
  "(P & (Q | R)) = ((P&Q) | (P&R))"
haftmann@54251
    24
  "((Q | R) & P) = ((Q&P) | (R&P))"
haftmann@54251
    25
  "(P \<and> Q) = (Q \<and> P)"
haftmann@54251
    26
  "(P \<or> Q) = (Q \<or> P)"
haftmann@36712
    27
  by blast+
haftmann@36712
    28
haftmann@36712
    29
lemmas weak_dnf_simps = dnf bool_simps
haftmann@36712
    30
haftmann@36712
    31
lemma PFalse:
haftmann@36712
    32
    "P \<equiv> False \<Longrightarrow> \<not> P"
haftmann@36712
    33
    "\<not> P \<Longrightarrow> (P \<equiv> False)"
haftmann@36712
    34
  by auto
haftmann@36712
    35
haftmann@36712
    36
ML {*
wenzelm@45294
    37
structure Algebra_Simplification = Named_Thms
wenzelm@45294
    38
(
wenzelm@45294
    39
  val name = @{binding algebra}
haftmann@36712
    40
  val description = "pre-simplification rules for algebraic methods"
haftmann@36712
    41
)
haftmann@28402
    42
*}
haftmann@28402
    43
haftmann@36712
    44
setup Algebra_Simplification.setup
haftmann@36712
    45
wenzelm@48891
    46
ML_file "Tools/groebner.ML"
haftmann@36751
    47
wenzelm@47432
    48
method_setup algebra = {*
wenzelm@47432
    49
  let
wenzelm@47432
    50
    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
wenzelm@47432
    51
    val addN = "add"
wenzelm@47432
    52
    val delN = "del"
wenzelm@47432
    53
    val any_keyword = keyword addN || keyword delN
wenzelm@47432
    54
    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
wenzelm@47432
    55
  in
wenzelm@47432
    56
    Scan.optional (keyword addN |-- thms) [] --
wenzelm@47432
    57
     Scan.optional (keyword delN |-- thms) [] >>
wenzelm@47432
    58
    (fn (add_ths, del_ths) => fn ctxt =>
wenzelm@47432
    59
      SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
wenzelm@47432
    60
  end
wenzelm@47432
    61
*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
haftmann@36751
    62
haftmann@36712
    63
declare dvd_def[algebra]
haftmann@36712
    64
declare dvd_eq_mod_eq_0[symmetric, algebra]
haftmann@36712
    65
declare mod_div_trivial[algebra]
haftmann@36712
    66
declare mod_mod_trivial[algebra]
huffman@47142
    67
declare div_by_0[algebra]
huffman@47142
    68
declare mod_by_0[algebra]
haftmann@36712
    69
declare zmod_zdiv_equality[symmetric,algebra]
huffman@47165
    70
declare div_mod_equality2[symmetric, algebra]
huffman@47159
    71
declare div_minus_minus[algebra]
huffman@47159
    72
declare mod_minus_minus[algebra]
huffman@47159
    73
declare div_minus_right[algebra]
huffman@47159
    74
declare mod_minus_right[algebra]
huffman@47142
    75
declare div_0[algebra]
huffman@47142
    76
declare mod_0[algebra]
haftmann@36712
    77
declare mod_by_1[algebra]
haftmann@36712
    78
declare div_by_1[algebra]
huffman@47160
    79
declare mod_minus1_right[algebra]
huffman@47160
    80
declare div_minus1_right[algebra]
haftmann@36712
    81
declare mod_mult_self2_is_0[algebra]
haftmann@36712
    82
declare mod_mult_self1_is_0[algebra]
haftmann@36712
    83
declare zmod_eq_0_iff[algebra]
haftmann@36712
    84
declare dvd_0_left_iff[algebra]
haftmann@36712
    85
declare zdvd1_eq[algebra]
haftmann@36712
    86
declare zmod_eq_dvd_iff[algebra]
haftmann@36712
    87
declare nat_mod_eq_iff[algebra]
haftmann@36712
    88
haftmann@28402
    89
end