Email Gateway (Aug 22 2022 at 14:18): Email Gateway (Aug 22 2022 at 14:18):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I just noticed the following odd behavior: the "algebra" proof method
seems to stop working whe ~/src/HOL/Algebra/Ring is imported. This does
not seem to be a regression either; the same problem occurred in
Isabelle2016.
Example:
theory Test
imports Main "~~/src/HOL/Algebra/Ring"
begin
lemma
fixes a b :: nat
shows "a * b = b * a" by algebra
end
(when the ~~/src/HOL/Algebra/Ring import is removed, everything works)
Any ideas, anyone?
Manuel
Email Gateway (Aug 22 2022 at 14:19):From: Manuel Eberl <eberlm@in.tum.de>
I decided to look into the matter myself after all and found the
problem: the "normal" algebra method we all know and love is declared in
"Groebner_Basis", but HOL-Algebra also declares an "algebra" method that
shadows the other one.
Of course, one can still access both of them using the fully-qualified
names Ring.algebra and Groebner_Basis.algebra. Still, in my opinion, it
may a good idea to resolve this naming conflict.
For instance, the situation is that currently, proofs using the
"algebra" method break once HOL-Number_Theory is imported (since it
depends on some theories from HOL-Algebra)
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 14:19):From: Lawrence Paulson <lp15@cam.ac.uk>
This conflict should indeed be resolved. The intention was for the original “algebra” method to be generalised to include other types of algebraic reasoning. The ideal solution would be for the other method (whatever it does) to extend rather than to replace the original one.
Larry
Last updated: Apr 20 2024 at 04:19 UTC