[isabelle] Record for module?



I need a record for a module but the *record module* in Module.thy actually
defines a record for an algebra instead (an algebra has multiplication, a
module does not) - so is a bit of a misnomer.

record ('a, 'b) module = "'b *ring*" +
  smult :: "['a, 'b] => 'b" (infixl "⊙ı" 70)
[note it's "ring" not "monoid"]

The *locale module* is correct but does not seem to have a record
associated with it.

I'm wondering whether I've missed it somewhere, or I need to define my own.
If I do formalise it myself (by changing "ring" to "monoid" above) will it
still be compatible with the locale module? As a side note, is it true that
a record can only "inherit" from one other record (so that there's no way
to have something like

record ('a, 'b) Module = "('a ring)" + "('b monoid)" +
  smult :: "['a, 'b] => 'b" (infixl "⊙ı" 70)

that would encapsulate both a ring and module?)

[I'm formalising vector spaces over an arbitrary field; a vector space is a
module where the ring is a field.]

(Thanks for all the helpful responses to my previous queries!)

-Holden



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