Relevant rules added to algebra's context
authorchaieb
Mon Jul 21 13:36:39 2008 +0200 (2008-07-21)
changeset 276661436d81d1294
parent 27665 b9e54ba563b3
child 27667 62500b980749
Relevant rules added to algebra's context
src/HOL/Groebner_Basis.thy
     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