[isabelle] abelian_group

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.