Email Gateway (Aug 18 2022 at 17:24): Email Gateway (Aug 18 2022 at 17:24):From: Steve W <s.wong.731@gmail.com>
Hi,
I'm looking at how "real_vector" is used as a type and am somewhat confused
by examples like:
definition
convex :: "'a::real_vector set \<Rightarrow> bool" ...
in HOL/Library/Convex.thy. How come "convex" is declared wrt the type
variable "'a" rather than "real_vector" directly, i.e.
convex :: "real_vector set..."
Thank you for any help.
Steve
Email Gateway (Aug 18 2022 at 17:24):From: Johannes Hölzl <hoelzl@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.
Hope this helps,
Johannes
Email Gateway (Aug 18 2022 at 17:25):From: Steve W <s.wong.731@gmail.com>
2011/3/22 Johannes Hölzl <hoelzl@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.
Thanks
Steve
Hope this helps,
JohannesAm Dienstag, den 22.03.2011, 16:54 +0000 schrieb Steve W:
Hi,
I'm looking at how "real_vector" is used as a type and am somewhat
confused
by examples like:definition
convex :: "'a::real_vector set \<Rightarrow> bool" ...in HOL/Library/Convex.thy. How come "convex" is declared wrt the type
variable "'a" rather than "real_vector" directly, i.e.convex :: "real_vector set..."
Thank you for any help.
Steve
Email Gateway (Aug 18 2022 at 17:25):From: Johannes Hölzl <hoelzl@in.tum.de>
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)
Email Gateway (Aug 18 2022 at 17:25):From: Brian Huffman <brianh@cs.pdx.edu>
2011/3/22 Johannes Hölzl <hoelzl@in.tum.de>:
Am Dienstag, den 22.03.2011, 17:37 +0000 schrieb Steve W:
2011/3/22 Johannes Hölzl <hoelzl@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,
Email Gateway (Aug 18 2022 at 17:25):From: Timothy McKenzie <tjm1983@gmail.com>
Do you mean this?
consts v :: "'a::real_vector"
Tim
<><
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC