Thanks, Michael. I have provided links and quotes from the source with
definitions below.
My knowledge on the technical details of the HOL/HOL4 implementation is limited.
Is it correct to say that 'a is the polymorphic type-variable, and that the
(monoid and) group definition is based on an ML d
You have misunderstood.
The Hol_datatype call establishes a type entirely within the logic and is *not*
an SML entity at all. The mathematical content is entirely within the logic.
The definition of Group that you found is expressed in terms of Monoid. (Every
group is a monoid.) The monoid typ
Thanks for the clarification that the Hol_datatype call establishes a type
entirely within the logic.
However, in HOL/HOL4 a natural expression of a statement such as Grp(Z,+) or
Grp(o, XOR) isn't possible for two reasons:
1. The group carrier set is represented at the type level only, but not
> I just want to point out that the goalposts have shifted
> slightly. The material pointed to by Michael shows that a fair
> bit of basic abstract algebra can be cleanly done in HOL's type
> theory, which I gather was the original point in question.
>
> re: Ken's questions.
>
> 1. The carrier is e
