[isabelle-dev] Application of method algebra fails

[christian at madez.de]

In some cases, the proof method algebra fails even though it should work.
The bug can be reproduced in one case with the following theory:

theory Scratch
  imports Main
begin

lemma "(- x + 3) * (x + 1) + (x - 1) ^ 2 - 3 = (1::int)"
  by algebra

lemma "(- x + 3) * (x + 1) + (x - 1) ^ 2 - 2 = (2::int)"
  by algebra

end
I verified the bug occurs on Isabelle2021-1, Isabelle2022 and on the changeset 77699:d5060a919b3f from Mon Mar 20 18:33:56 2023 +0100.

CTRL + left click on the proof method algebra in Isabelle opens the file src/HOL/Groebner_Basis.thy. This points to algebra_tac in Tools/groebner.ML. There we find the definition

fun algebra_tac add_ths del_ths ctxt i =
 ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i
We can find the definition of ring_tac in the same file as:

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230322/6238a993/attachment.htm>