Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Record for module?

Email Gateway (Aug 19 2022 at 14:54):

From: Holden Lee <hl422@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

Email Gateway (Aug 19 2022 at 14:55):

From: Holden Lee <hl422@cam.ac.uk>
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.)

-Holden

Email Gateway (Aug 19 2022 at 14:56):

From: Clemens Ballarin <ballarin@in.tum.de>
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@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

Last updated: May 01 2024 at 20:18 UTC