src/HOL/Groebner_Basis.thy
 changeset 27666 1436d81d1294 parent 26462 dac4e2bce00d child 28402 09e4aa3ddc25
```     1.1 --- a/src/HOL/Groebner_Basis.thy	Sun Jul 20 23:07:03 2008 +0200
1.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Jul 21 13:36:39 2008 +0200
1.3 @@ -13,7 +13,6 @@
1.4    ("Tools/Groebner_Basis/groebner.ML")
1.5  begin
1.6
1.7 -
1.8  subsection {* Semiring normalization *}
1.9
1.10  setup NormalizerData.setup
1.11 @@ -251,6 +250,7 @@
1.12
1.13  use "Tools/Groebner_Basis/normalizer.ML"
1.14
1.15 +
1.16  method_setup sring_norm = {*
1.17    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt))
1.18  *} "semiring normalizer"
1.19 @@ -415,7 +415,6 @@
1.20      "P \<equiv> False \<Longrightarrow> \<not> P"
1.21      "\<not> P \<Longrightarrow> (P \<equiv> False)"
1.22    by auto
1.23 -
1.24  use "Tools/Groebner_Basis/groebner.ML"
1.25
1.26  method_setup algebra =
1.27 @@ -434,5 +433,32 @@
1.28         Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
1.29  end
1.30  *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
1.31 +declare dvd_def[algebra]
1.32 +declare dvd_eq_mod_eq_0[symmetric, algebra]
1.33 +declare nat_mod_div_trivial[algebra]
1.34 +declare nat_mod_mod_trivial[algebra]
1.35 +declare conjunct1[OF DIVISION_BY_ZERO, algebra]
1.36 +declare conjunct2[OF DIVISION_BY_ZERO, algebra]
1.37 +declare zmod_zdiv_equality[symmetric,algebra]
1.38 +declare zdiv_zmod_equality[symmetric, algebra]
1.39 +declare zdiv_zminus_zminus[algebra]
1.40 +declare zmod_zminus_zminus[algebra]
1.41 +declare zdiv_zminus2[algebra]
1.42 +declare zmod_zminus2[algebra]
1.43 +declare zdiv_zero[algebra]
1.44 +declare zmod_zero[algebra]
1.45 +declare zmod_1[algebra]
1.46 +declare zdiv_1[algebra]
1.47 +declare zmod_minus1_right[algebra]
1.48 +declare zdiv_minus1_right[algebra]
1.49 +declare mod_div_trivial[algebra]
1.50 +declare mod_mod_trivial[algebra]
1.51 +declare zmod_zmult_self1[algebra]
1.52 +declare zmod_zmult_self2[algebra]
1.53 +declare zmod_eq_0_iff[algebra]
1.54 +declare zdvd_0_left[algebra]
1.55 +declare zdvd1_eq[algebra]
1.56 +declare zmod_eq_dvd_iff[algebra]
1.57 +declare nat_mod_eq_iff[algebra]
1.58
1.59  end
```