Re: [isabelle] abelian_group

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

Kind regards,
Slawomir Kolodynski Library of Formalized Mathematics for Isabelle/Isar (ZF Logic) 
   On Friday, April 12, 2019, 6:21:19 PM GMT+2, Manuel Eberl <eberlm at> 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.


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)"


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