<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<div dir="auto">In some cases, the proof method algebra fails even though it should work.<br></div><div dir="auto">The bug can be reproduced in one case with the following theory:<br></div><div dir="auto"><br></div><div dir="auto">theory Scratch<br> imports Main<br>begin<br><br>lemma "(- x + 3) * (x + 1) + (x - 1) ^ 2 - 3 = (1::int)"<br> by algebra<br><br>lemma "(- x + 3) * (x + 1) + (x - 1) ^ 2 - 2 = (2::int)"<br> by algebra<br><br>end</div><div dir="auto"><br></div><div dir="auto">I verified the bug occurs on Isabelle2021-1, Isabelle2022 and on the changeset 77699:d5060a919b3f from Mon Mar 20 18:33:56 2023 +0100.<br></div><div dir="auto"><br></div><div dir="auto">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<br></div><div dir="auto"><br></div><div dir="auto">fun algebra_tac add_ths del_ths ctxt i =<br> ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i</div><div dir="auto"><br></div><div dir="auto">We can find the definition of ring_tac in the same file as:<br></div><div dir="auto"><br></div> </body>
</html>