[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
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 =
  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

Best regards


*PhD. Anthony Bordg*

*Postdoctoral Research Associate*

*Cambridge University, UKhttps://sites.google.com/site/anthonybordg/

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