[isabelle-dev] NEWS

[Amine Chaieb]

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.