# [isabelle] HOL-Algebra

Dear all,
I noticed something weird with the definition of abelian monoids in
the Ring theory of the HOL-Algebra library.
Indeed, there one can find the following locale:
locale abelian_monoid =
fixes G (structure)
assumes a_comm_monoid:
"comm_monoid (add_monoid G)"
, and if one hovers over the G variable (with the cmd key) then one
notices that it is of type "('a, 'b) ring-scheme".
As a consequence, one needs a ring-scheme to define an abelian monoid!
Is there any good reason for that choice ?
Let assume that I need to prove that the set of 4-dimensional real
vectors, equipped with the obvious addition and zero, is an abelian
monoid,
do you suggest me to use the following record:
definition real4_monoid :: "(_, _) ring_scheme" where
"real4_monoid ≡ ⦇carrier = UNIV::(real^4) set, mult = real4_add, one =
real4_zero,
zero = undefined, add = undefined⦈" ?
Of course, the necessary (due to the fact noticed above) hack of using
"undefined" is not elegant, so one may want to fix the Algebra
library.
Best regards
Anthony
--
*PhD. Anthony Bordg*
*Postdoctoral Research Associate*
*Cambridge University, UKhttps://sites.google.com/site/anthonybordg/
<https://sites.google.com/site/anthonybordg/>*

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