Re: [isabelle] Record for module?



Hi Holden,

The problem is that records can only be extended by adding elements.  There is no multiple inheritance.  That is, it is not possible to extend the monoid record by scalar multiplication and then later join in with the ring record.  But this is not a big issue.  \<otimes> is simply not specified for the module locale.

> It seems that the reason for this is to use the additive \oplus notation
> for module rather than \otimes. (Monoid uses \otimes, and it seems that
> once the notation is chosen it cannot be changed.)

A distinctive feature of the record approach is that notation is fixed (and one needs to rely on subscripts if necessary).  In an algebra you have two proper multiplications, \<otimes>_R and \<otimes>_M and a single multiplication by a scalar \<odot>_M.

Clemens

> 2014-07-16 18:28 GMT+01:00 Holden Lee <hl422 at cam.ac.uk>:
>
> > 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.