Re: [isabelle] abelian_group
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
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)
"comm_monoid (add_monoid G)"
locale abelian_group = abelian_monoid +
"comm_group (add_monoid G)"
This archive was generated by a fusion of
Pipermail (Mailman edition) and