src/HOL/Groebner_Basis.thy
 author haftmann Sun May 06 18:20:25 2018 +0000 (12 months ago) changeset 68100 b2d84b1114fa parent 67091 1393c2340eec child 68484 59793df7f853 permissions -rw-r--r--
removed some lemma duplicates
```     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) \<comment> \<open>FIXME move to @{theory HOL}\<close>
```
```    14
```
```    15 lemma nnf_simps: \<comment> \<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 \<and> (Q \<or> R)) = ((P\<and>Q) \<or> (P\<and>R))"
```
```    23   "((Q \<or> R) \<and> P) = ((Q\<and>P) \<or> (R\<and>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.repeats (Scan.unless any_keyword Attrib.multi_thm);
```
```    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 mod_eq_0_iff_dvd[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 mult_div_mod_eq[algebra]
```
```    60 declare div_minus_minus[algebra]
```
```    61 declare mod_minus_minus[algebra]
```
```    62 declare div_minus_right[algebra]
```
```    63 declare mod_minus_right[algebra]
```
```    64 declare div_0[algebra]
```
```    65 declare mod_0[algebra]
```
```    66 declare mod_by_1[algebra]
```
```    67 declare div_by_1[algebra]
```
```    68 declare mod_minus1_right[algebra]
```
```    69 declare div_minus1_right[algebra]
```
```    70 declare mod_mult_self2_is_0[algebra]
```
```    71 declare mod_mult_self1_is_0[algebra]
```
```    72 declare zmod_eq_0_iff[algebra]
```
```    73 declare dvd_0_left_iff[algebra]
```
```    74 declare zdvd1_eq[algebra]
```
```    75 declare mod_eq_dvd_iff[algebra]
```
```    76 declare nat_mod_eq_iff[algebra]
```
```    77
```
```    78 context semiring_parity
```
```    79 begin
```
```    80
```
```    81 declare even_mult_iff [algebra]
```
```    82 declare even_power [algebra]
```
```    83
```
```    84 end
```
```    85
```
```    86 context ring_parity
```
```    87 begin
```
```    88
```
```    89 declare even_minus [algebra]
```
```    90
```
```    91 end
```
```    92
```
```    93 declare even_Suc [algebra]
```
```    94 declare even_diff_nat [algebra]
```
```    95
```
```    96 end
```