chaieb at in.tum.de
Wed Oct 31 12:21:00 CET 2007
The method algebra has been extended to solve a generalized version of
the ideal membership problem (cf. ) over rings. This new feature is
also "localic" as the old method algebra.
Here is an example (from )
lemma "EX (d::int). a*y - a*x = n*d ==> EX u v. a*u + n*v = 1 ==> EX e.
y - x = n*e"
This expresses for instance the follwing cancellation law:
"ALL a n x y. a*x = a*y (mod n) & coprime a n --> x = y (mod n)"
see  for more interesting number-theoretic applications.
The general problem solved by this extension is
ALL x1 ... xn. p1(x1,...,xn) = 0 & ..., pm(x1,...,xn) = 0 --->
EX y1 ... yk. q11(x1,..,xn)*y1 + ... + q1r(x1,...,xn)*yk = 0 &
qt1(x1,...,xn)*y1 + ... + qtr(x1,...,xn)*yk = 0
: John Harrison, Automating elementary number-theoretic proofs using
Groebner bases, CADE 2007.
More information about the isabelle-dev