*To*: sudbrock at cs.tu-darmstadt.de*Subject*: Re: [isabelle] Working with Vector Spaces*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Fri, 13 Aug 2010 11:56:58 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20100812172018.2f90f6f9@mio>*Organization*: Technische Universität München*References*: <20100812172018.2f90f6f9@mio>

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 > >

**References**:**[isabelle] Working with Vector Spaces***From:*sudbrock

- Previous by Date: Re: [isabelle] Unfolding setsum
- Next by Date: Re: [isabelle] simple proof question
- Previous by Thread: [isabelle] Working with Vector Spaces
- Next by Thread: [isabelle] Comparing square roots
- Cl-isabelle-users August 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list