Re: [isabelle] abelian_group



Hi Dominique,

> 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 do not say that this is not possible, but IMHO there are too many open
questions to tackle that on one step;  the existing algebraic type class
hierarchy is essential for the HOL bootstrap e.g. wrt. numeric types
without subtyping.  Personally I got used to view the class / locale
dichotomy (which carries over to the sessions distinctive HOL-Algebra
and HOL-Computational_Algebra) as an inherent consequence of Isabelle's
higher-order logic »as it is«.

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

There is some danger to reproduce the situation with
(Old/New)_Number_Theory as it was from 2009 until 2016.

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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