# [isabelle] Working with Vector Spaces

```Hi all,

I am looking for a way to define algebraic structures
like, for instance, modules over rings or vector spaces
over fields in Isabelle/HOL. In particular, I want to
formulate statements like the following: "The product of
two vector spaces over a field K is a vector space over
the field K."

As far as I see, this is possible using 'typedef' to
define a type as follows (for vector spaces):

typedef ('K, 'V) vectorspace = "{
(zero :: 'V,
add :: 'V => 'V => 'V,
inverse :: 'V => 'V,
scalarmult :: 'K => 'V => 'V
(* ... *)
(ALL v. (add v zero) = v)
(* ... *)
}"

As working with typedef-ed types seems somewhat
cumbersome, and concepts like Haskell-style type classes
or locales seem to be useful for algebraic structures (as
algebraic structures are used in the running examples in
the documentation), I am wondering if I should rather use
one of those two concepts.

However, as far as I found out, type classes support only
one type parameter (while I need two, one for the
underlying ring/field, and one for the abelian group of
the module/vector space). Is there a reason for this
restriction of type classes?

Concerning locales, I found the vectorspace-locale of the
HahnBanach-theory within the Isabelle library. However, I
do not see how to define functions like "the product of
two vector spaces" (which would map two instantiations of
the locale to a third instantiation of the locale) for
such a locale. Is there any way to define such functions?

Or is there perhaps another "standard" or "recommended"
way to define such structures in Isabelle/HOL?

Best regards,
Henning

--
Henning Sudbrock

Modeling and Analysis of Information Systems
Department of Computer Science, TU Darmstadt
Hochschulstraße 10