*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Working with Vector Spaces*From*: sudbrock at cs.tu-darmstadt.de*Date*: Thu, 12 Aug 2010 17:20:18 +0200*Organization*: MAIS, FB Informatik, TU Darmstadt

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

**Follow-Ups**:**Re: [isabelle] Working with Vector Spaces***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] class instance of a record extension
- Next by Date: [isabelle] Comparing square roots
- Previous by Thread: Re: [isabelle] class instance of a record extension
- Next by Thread: Re: [isabelle] Working with Vector Spaces
- 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