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