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, ...
  assumes "..."

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


lemma vector_space_product:
  assumes "vector_space z1 add1 ..."
  assumes "vector_space z2 add2 ..."
  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"

See also src/HOL/Algebra for application of locales to algebraic
structures.

Greetings,
  Johannes


> Best regards,
> Henning
> 
> 







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