*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] abelian_group*From*: Slawomir Kolodynski via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Date*: Sat, 13 Apr 2019 07:13:28 +0000 (UTC)*In-reply-to*: <cab8db41-0746-f1c2-f5bf-d6f7a5bae524@in.tum.de>*References*: <A80C58ED-7E98-4574-9A67-7CA0259B6885@cam.ac.uk> <cab8db41-0746-f1c2-f5bf-d6f7a5bae524@in.tum.de>*Reply-to*: Slawomir Kolodynski <skokodyn at yahoo.com>

Hi Manuel, > as far as I know, it's the only way we have in Isabelle to do abstract algebra I assume you mean Isabelle/HOL here. In IsarMathLib notation details are deferred to the presentation layer so they are not tied to definitions. Multiplicative notation happens to be used in context of semigroups, groups and abelian groups, while additive notation is used for abelian semigroups and topological groups (see Semigroup_ZF, Group_ZF, AbelianGroup_ZF and CommutativeSemigroup_ZF, TopologicalGroup_ZF at isarmathlib.org ). Kind regards, Slawomir Kolodynski http://savannah.nongnu.org/projects/isarmathlib Library of Formalized Mathematics for Isabelle/Isar (ZF Logic) On Friday, April 12, 2019, 6:21:19 PM GMT+2, Manuel Eberl <eberlm at in.tum.de> wrote: HOL-Algebra is a bit messy. A big part of that, I think, comes from quirks of Isabelle/HOL itself. My guess would be that one can write groups either additively (G, +, 0) or multiplicatively (G, *, 1). Of course, more abstract syntax (G, ∘, e) is also possible. There are various conventions about when to use which notation – in particular, I think the convention is that if you use "+", the group is always commutative (i.e. abelian). In HOL-Algebra, groups are /always/ written multiplicatively. There is no other way. When you have a ring, you can write "+" for addition, but that is not formally associated to any group. The additive group of the ring has all its properties stated w.r.t. the "*" of "add_monoid R". "abelian_group" is apparently some kind of attempt to have an abelian group that is written additively. Due to the fact that the "+" operator is defined for the ring record, this requires us to use a ring record even though there is (in general) no multiplication operation. We also don't have any locale assumption that this "ring record" is an actual ring (i.e. fulfils the ring axioms). Just the addition operation in it is required to form an abelian group. As for why this strange "abelian_group" locale exists, I cannot say. One would have to examine where it is used and what for. I agree that it's all very confusing. Maybe it is simply the case that this ad-hoc "single-inheritance record" "locale with structure parameters" is just fraught with problems. But as far as I know, it's the only way we have in Isabelle to do abstract algebra, and I don't know of a better one. Unless we can find a way to emulate the more modular typeclass/implicit parameter approach and elaborators that systems like Coq and Lean have. Manuel On 12/04/2019 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)" > >

**References**:**[isabelle] abelian_group***From:*Lawrence Paulson

**Re: [isabelle] abelian_group***From:*Manuel Eberl

- Previous by Date: [isabelle] on formalization of predicate abstraction in Isabelle
- Next by Date: Re: [isabelle] abelian_group
- Previous by Thread: Re: [isabelle] abelian_group
- Next by Thread: [isabelle] Natural expression of group theory – Re: abelian_group
- Cl-isabelle-users April 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list