*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] HOL-Algebra breaks "algebra" method*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Fri, 21 Oct 2016 11:47:56 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <e8ee2fcc-4cf2-c228-0f03-14dcae64fee2@in.tum.de>*References*: <cf8a0040-5da5-55a5-1c52-123940487498@in.tum.de> <e8ee2fcc-4cf2-c228-0f03-14dcae64fee2@in.tum.de>

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 >> >

**References**:**[isabelle] HOL-Algebra breaks "algebra" method***From:*Manuel Eberl

**Re: [isabelle] HOL-Algebra breaks "algebra" method***From:*Manuel Eberl

- Previous by Date: [isabelle] AFP: LOFT
- Next by Date: Re: [isabelle] [ExternalEmail] Isabelle document prep and ACM journals document class
- Previous by Thread: Re: [isabelle] HOL-Algebra breaks "algebra" method
- Next by Thread: [isabelle] Haskell code generation for Imperative/HOL
- Cl-isabelle-users October 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list