[isabelle-dev] Application of method algebra fails
christian at madez.de
christian at madez.de
Wed Mar 22 23:50:45 CET 2023
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>
More information about the isabelle-dev
mailing list