Re: [isabelle] HOL-Algebra breaks "algebra" method



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

> On 21 Oct 2016, at 07:54, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> 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
> 
> 
> On 20/10/16 15:50, Manuel Eberl wrote:
>> 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
>> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.