[isabelle-dev] NEWS
Amine Chaieb
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. [1]) over rings. This new feature is
also "localic" as the old method algebra.
Here is an example (from [1])
lemma "EX (d::int). a*y - a*x = n*d ==> EX u v. a*u + n*v = 1 ==> EX e.
y - x = n*e"
by algebra
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 [1] 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
Amine.
[1]: John Harrison, Automating elementary number-theoretic proofs using
Groebner bases, CADE 2007.
More information about the isabelle-dev
mailing list