Re: [isabelle] abelian_group
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
o For transferring from locale to class, that might work
automatically (haven't checked) if we prove "sublocale XXX <=
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
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".)
This archive was generated by a fusion of
Pipermail (Mailman edition) and