Re: [isabelle] real_vector

2011/3/22 Johannes Hölzl <hoelzl at>:
> Am Dienstag, den 22.03.2011, 17:37 +0000 schrieb Steve W:
>> 2011/3/22 Johannes Hölzl <hoelzl at>
>> > 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

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