# Re: [isabelle] real_vector

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.
it is enough to say:
consts v :: "'a real_vector"
This is a constant of a arbitrary type forming a real vector space.
For example you can now write:
"v + sin 1"
in this case 'v' will be of type real.
Or you write
"case v of (a, b) => ..."
in this case it will be (real * real).
2) To have a vector of a specific size, you need to encode this in the
type. For example the HOL-Multivariate_Analysis image contains the
cartesian products:
real ^ 'n
Here 'n encodes the size as a type. (This is a restriction, but often
one can work around it)
- Johannes

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