*To*: Steve W <s.wong.731 at gmail.com>, Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] real_vector*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 22 Mar 2011 14:18:50 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1300817994.2260.467.camel@macbroy12.informatik.tu-muenchen.de>*References*: <AANLkTikwauGryS4pEXSt1t-K+cGw0yXDBP8JT_beW6xt@mail.gmail.com> <1300814308.2260.443.camel@macbroy12.informatik.tu-muenchen.de> <AANLkTimFEtAjcGJ8yDaCitvoi84voA_=2JHLz2LSk419@mail.gmail.com> <1300817994.2260.467.camel@macbroy12.informatik.tu-muenchen.de>*Sender*: huffman.brian.c at gmail.com

2011/3/22 Johannes Hölzl <hoelzl at in.tum.de>: > Am Dienstag, den 22.03.2011, 17:37 +0000 schrieb Steve W: >> 2011/3/22 Johannes Hölzl <hoelzl at in.tum.de> >> >> > real_vector is a type class, i.e. there are different types implementing >> > a real_vector. For example real, complex, real^'n, (real * real) are all >> > real vectors. >> > >> > So "'a :: real_vector set" is a set of type 'a where 'a forms a real >> > vector space. Hence convex is defined for real, real^'n, real * real, >> > etc. >> > >> >> I see. So if I'd like, say, a const v to be a real vector of reals, how do I >> go about that? 'consts v :: "real real_vector"' doesn't seem to be right. > > I'm not sure what you mean. > > 1) The types in the type class real_vector only contain vectors of > reals. So it is not necessary to specify this explicitly. Just to be clear: class "real_vector" includes finite-dimensional real vector spaces like "real * real" and "real ^ 'n", but it doesn't rule out the possibility of infinite-dimensional spaces (although I don't think there are any examples of such in the libraries yet). If you want to define operations on or prove lemmas about arbitrary *finite*-dimensional spaces, you can use the class "euclidean_space", which is defined in the Multivariate_Analysis theories. I think this might correspond more closely to what you mean by a "vector of reals". > it is enough to say: > > consts v :: "'a real_vector" > > This is a constant of a arbitrary type forming a real vector space. Actually, this contains a typo; it should be consts v :: "'a::real_vector" with a double-colon between the type variable and the class name. Without the double-colon, Isabelle will think that "real_vector" is supposed to be a type constructor, which it is not. I think some of the confusion might come from the somewhat unusual parsing rules for type application vs. sort annotations. The infix "::" for sort annotations actually binds more tightly than type constructor application, so the type expression "'a::real_vector set => bool" is actually parsed as "('a::real_vector) set => bool" It is *not* parsed as "'a::(real_vector set) => bool", which wouldn't make sense anyway. I admit this is rather confusing, especially since "::" binds quite loosely when it is used for type annotations on terms. Hope this helps, - Brian

**References**:**[isabelle] real_vector***From:*Steve W

**Re: [isabelle] real_vector***From:*Johannes Hölzl

**Re: [isabelle] real_vector***From:*Steve W

**Re: [isabelle] real_vector***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] real_vector
- Next by Date: Re: [isabelle] real_vector
- Previous by Thread: Re: [isabelle] real_vector
- Next by Thread: Re: [isabelle] real_vector
- Cl-isabelle-users March 2011 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