Re: [isabelle] real_vector
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and