Re: [isabelle] Working with Vector Spaces
Am Donnerstag, den 12.08.2010, 17:20 +0200 schrieb
sudbrock at cs.tu-darmstadt.de:
> 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 =
fixes zero, add, ...
To prove that a product of two vector spaces is again a vector space,
you can use the predicates:
assumes "vector_space z1 add1 ..."
assumes "vector_space z2 add2 ..."
shows "vector_space (z1, z2) ..."
(* 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 ...
> 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
Often the locale parameters for algebraic structures are packaged into a
record 'v 'k vector_space = 'v monoid +
scalar :: "'k => 'v => 'v"
See also src/HOL/Algebra for application of locales to algebraic
> Best regards,
This archive was generated by a fusion of
Pipermail (Mailman edition) and