# Re: [isabelle] Working with Vector Spaces

```Am Donnerstag, den 12.08.2010, 17:20 +0200 schrieb
> 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."
[..]
> 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?

When you use locales you get a predicate which describes your locale.

locale vector_space =
assumes "..."

To prove that a product of two vector spaces is again a vector space,
you can use the predicates:

lemma vector_space_product:
shows "vector_space (z1, z2) ..."
proof -
(* Use interpret to get all you locale lemmas and definitions *)
interpret vs1: vector_space z1 add1 ... by fact
interpret vs2: vector_space z2 add2 ... by fact

...
show ?thesis ...
qed

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

The recommended way is to use locales. Even type classes are based on
locales.

Often the locale parameters for algebraic structures are packaged into a
record:

record 'v 'k vector_space = 'v monoid +
scalar :: "'k => 'v => 'v"

structures.

Greetings,
Johannes

> Best regards,
> Henning
>
>

```

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