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.