# Re: [isabelle] abelian_group

Hi,

that's interesting. It would certainly be of interest to think of a
large-scale overhaul of HOL-Algebra using modern locale features.

`There is the additional problem that there is a lot of duplication of
``concepts, using classes vs locales.
`

`E.g., monoid_mult (type class, in HOL) vs. monoid (locale, in
``HOL-Algebra). The classes have the advantage of being easier to use than
``locales in many cases (at least I feel that way), but they have the
``limitation of always having UNIV as the carrier.
`

`As far as I know, all proofs are simply done twice. And someone building
``a development on these things needs to pick on approach and is then
``"locked in", which is problematic, since some material is only available
``in the HOL approach and some only in the HOL-Algebra approach.
`
In case of an overhaul, perhaps these concepts could be unified as well?

`I am not sure what the best approach is for such a unification, but some
``idea would be:
`
* Have compatible names as far as possible. E.g., if the class is
called XXX, then the locale is called l_XXX or something.
* Have the possibility to transfer theorems between compatible classes
and locales. (Compatible means: when the class is the locale with
carrier:=UNIV.)
o For transferring from locale to class, that might work
automatically (haven't checked) if we prove "sublocale XXX <=
l_XXX UNIV".
o For transferring from class to locale it more difficult.
Possibly something involving the Types_To_Sets tools might work?

Unfortunately, I fear that even though there is not /that/ much material
building on HOL-Algebra, it would involve a lot of work.

`What if instead of editing HOL-Algebra, a new session HOL-Algebra2 is
``created? And then deprecating HOL-Algebra. (Or even renaming HOL-Algebra
``to HOL-Algebra-Old.)
`
Then it will be optional to update old AFP material building on HOL-Algebra.

I also don't think there are any "heavy" users of HOL-Algebra these days

`I wonder whether that might partially be because of the incompatibility
``with the type-class approach. (I, at least, never look at HOL-Algebra
``because we are building on real_vector_space in our formalizations and
``thus "locked in".)
`
Best wishes,
Dominique.

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