# 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 \<longleftrightarrow> a = r0"
+proof-
+  have "a = r0 \<longleftrightarrow> add x a = add x r0" by (simp add: add_cancel)
+  thus "x = add x a \<longleftrightarrow> 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 \<longleftrightarrow> 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) \<noteq> 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