[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)
  & (ALL v v'. (add v v') = (add v' 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 Sudbrock

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

Tel. 06151-16-6216
Fax. 06151-16-5326

E-Mail sudbrock at cs.tu-darmstadt.de

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