Re: [isabelle] abelian_group

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.


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?


record 'a ring = "'a monoid" +
  zero :: 'a ("𝟬ı")
  add :: "['a, 'a] ⇒ 'a" (infixl "⊕ı" 65)

  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.