# HG changeset patch # User chaieb # Date 1193829575 -3600 # Node ID b3a485b98963e6c45b48564a06b2b8a9eca175e1 # Parent 76b9892020d52479052099206dd3f079a22b991a (1) added axiom to ringb and theorems to enable algebra to prove the ideal membership problem; (2) Method algebra now calls algebra_tac which first tries to solve a universal formula, then in case of failure trie to solve the ideal membership problem (see HOL/Tools/Groebner_Basis/groebner.ML) diff -r 76b9892020d5 -r b3a485b98963 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Wed Oct 31 12:19:33 2007 +0100 +++ b/src/HOL/Groebner_Basis.thy Wed Oct 31 12:19:35 2007 +0100 @@ -301,6 +301,12 @@ thus "False" using add_mul_solve nz cnd by simp qed +lemma add_r0_iff: " x = add x a \ a = r0" +proof- + have "a = r0 \ add x a = add x r0" by (simp add: add_cancel) + thus "x = add x a \ a = r0" by (auto simp add: add_c add_0) +qed + declare "axioms" [normalizer del] lemma "axioms" [normalizer @@ -311,7 +317,8 @@ end -locale ringb = semiringb + gb_ring +locale ringb = semiringb + gb_ring + + assumes subr0_iff: "sub x y = r0 \ x = y" begin declare "axioms" [normalizer del] @@ -321,11 +328,13 @@ semiring rules: semiring_rules ring ops: ring_ops ring rules: ring_rules - idom rules: noteq_reduce add_scale_eq_noteq]: + idom rules: noteq_reduce add_scale_eq_noteq + ideal rules: subr0_iff add_r0_iff]: "ringb add mul pwr r0 r1 sub neg" by fact end + lemma no_zero_divirors_neq0: assumes az: "(a::'a::no_zero_divisors) \ 0" and ab: "a*b = 0" shows "b = 0" @@ -349,7 +358,6 @@ thus "w = x" by simp qed - declaration {* normalizer_funs @{thm class_ringb.axioms} *} interpretation natgb: semiringb @@ -386,7 +394,8 @@ semiring rules: semiring_rules ring ops: ring_ops ring rules: ring_rules - idom rules: noteq_reduce add_scale_eq_noteq]: + idom rules: noteq_reduce add_scale_eq_noteq + ideal rules: subr0_iff add_r0_iff]: "fieldgb add mul pwr r0 r1 sub neg divide inverse" by unfold_locales end @@ -424,8 +433,8 @@ ((Scan.optional (keyword addN |-- thms) []) -- (Scan.optional (keyword delN |-- thms) [])) src #> (fn ((add_ths, del_ths), ctxt) => - Method.SIMPLE_METHOD' (Groebner.ring_tac add_ths del_ths ctxt)) + Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt)) end -*} "solve polynomial equations over (semi)rings using Groebner bases" +*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" end