Re: [isabelle] abelian_group

Hello Clemens,

that's interesting. It would certainly be of interest to think of a
large-scale overhaul of HOL-Algebra using modern locale features.
Unfortunately, I fear that even though there is not /that/ much material
building on HOL-Algebra, it would involve a lot of work.

I also don't think there are any "heavy" users of HOL-Algebra these days
who could champion such an endeavour and come up with better designs. If
there are – please come forward! (Larry had two students who might
actually be the two heaviest recent users.

I've used HOL-Algebra sporadically over the last two years or so and
would like to see it improved. Unfortunately, I do not have the time to
do that myself in the foreseeable future, and I also don't think I am an
ideal candidate to do it considering my lack of expertise with
HOL-Algebra and locales.


On 12/04/2019 22:36, Clemens Ballarin wrote:
> Hi Larry,
> when reading HOL-Algebra you need to keep in mind that much of the
> material pre-dates modern locales.  Then locales were not based on
> local theories, and expressions were limited to renaming;
> instantiation and rewriting were unavailable.
> The approach of combining locales with records dates back to that
> time.  Definitions in locales were unavailable, and the solution was
> to extract the signature part of an algebraic structure into a record,
> on which definitions could be made globally.  Locales would only deal
> with the specification part.
> Regarding the locale abelian_group: an abelian group by convention is
> a commutative group with additive notation.  A ring then is a
> (multiplicative) monoid and an abelian group.  What you see is an
> attempt of expressing that.  Unfortunately, since there isn't multiple
> inheritance for records, I needed to resort to using the ring record
> also for abelian groups, which is, of course, awkward.
> Clemens
> On 2019-04-12 17:01, Lawrence Paulson wrote:
>> A notable peculiarity of Algebra is its locale abelian_group, which is
>> based on comm_group (groups with commutative multiplication) but with
>> the weird twist of requiring a ring; it appears to be, in reality, the
>> specification that a ring’s addition operator is commutative. Except
>> that all rings have this property, and the very existence of this
>> locale is confusing. Does anybody know any more about this?
>> Larry
>> record 'a ring = "'a monoid" +
>>   zero :: 'a ("𝟬ı")
>>   add :: "['a, 'a] ⇒ 'a" (infixl "⊕ı" 65)
>> abbreviation
>>   add_monoid :: "('a, 'm) ring_scheme ⇒ ('a, 'm) monoid_scheme"
>>   where "add_monoid R ≡ ⦇ carrier = carrier R, mult = add R, one =
>> zero R, … = (undefined :: 'm) ⦈"
>> locale abelian_monoid =
>>   fixes G (structure)
>>   assumes a_comm_monoid:
>>      "comm_monoid (add_monoid G)"
>> locale abelian_group = abelian_monoid +
>>   assumes a_comm_group:
>>      "comm_group (add_monoid G)"

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