Email Gateway (Aug 18 2022 at 15:24): Email Gateway (Aug 18 2022 at 15:24):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Isabelle Users
If A and B are sets, direct sum C of A and B is a set of pairs (a, b) where a \in A and b \in B.
My first question – is this direct sum defined somewhere in Isabelle?
Now, in my case A is a subset of R^n and B is a subset of R^m. In this case, clearly, C is a subset of R^{n+m}. Currently, finite Cartesian product R^n formalized as type real^'n where 'n is some finite type. Now, is it possible to say that C is a subset of real^('n+'m) ? It seems that I can add types (theory Sum_Type), so I would imagine definition of direct sum as a function from (real^'n, real^'m) to real^('n+'m) such that first n coordinates of sum(x, y) coincides with x, and the next m coordinates - with y. Any ideas how to write down such a definition, which theories to look at, or may be suggestions how to formalize this in a different, more convenient way, would be appreciated.
Sincerely,
Bogdan Grechuk
Email Gateway (Aug 18 2022 at 15:24):From: Tobias Nipkow <nipkow@in.tum.de>
grechukbogdan schrieb:
Dear Isabelle Users
If A and B are sets, direct sum C of A and B is a set of pairs (a, b) where a \in A and b \in B.
My first question – is this direct sum defined somewhere in Isabelle?
Yes. It is written "A <> B". See Product_Type.thy. (Search for "<>")
Now, in my case A is a subset of R^n and B is a subset of R^m. In this case, clearly, C is a subset of R^{n+m}.
I'm afraid not the way that these types are defined in HOL. C is only
isomorphic to R^(n+m). You can spell out the type isomorphism explicitly
or define a special product construction on finite Cartesian products.
In either case I leave it to the experts to show you how to do it.
Tobias
Currently, finite Cartesian product R^n formalized as type real^'n where 'n is some finite type. Now, is it possible to say that C is a subset of real^('n+'m) ? It seems that I can add types (theory Sum_Type), so I would imagine definition of direct sum as a function from (real^'n, real^'m) to real^('n+'m) such that first n coordinates of sum(x, y) coincides with x, and the next m coordinates - with y. Any ideas how to write down such a definition, which theories to look at, or may be suggestions how to formalize this in a different, more convenient way, would be appreciated.
Sincerely,
Bogdan Grechuk
Email Gateway (Aug 18 2022 at 15:25):From: Lawrence Paulson <lp15@cam.ac.uk>
Once again, this formalisation of finite Cartesian products is showing itself to be unsuitable for abstract mathematics. It is only useful if you intend to work in one fixed dimension. I hope it isn't used extensively.
Larry
Email Gateway (Aug 18 2022 at 15:25):From: Tobias Nipkow <nipkow@in.tum.de>
Lawrence Paulson schrieb:
Once again, this formalisation of finite Cartesian products is showing itself to be unsuitable for abstract mathematics.
I'm interested: how do you model the problem in any formalism such that
A^m * B^n = A^(m+n) without resorting to an explicit isomorphism along
the way? Unless I am mistaken, the datatypes you provide in your
formalization of ZF do not do the job either.
It is only useful if you intend to work in one fixed dimension. I hope it isn't used extensively.
It is. Luckily it works quite well for concrete mathematics.
Tobias
Larry
On 28 Jun 2010, at 17:56, grechukbogdan wrote:
If A and B are sets, direct sum C of A and B is a set of pairs (a, b) where a \in A and b \in B.
My first question – is this direct sum defined somewhere in Isabelle?Now, in my case A is a subset of R^n and B is a subset of R^m. In this case, clearly, C is a subset of R^{n+m}. Currently, finite Cartesian product R^n formalized as type real^'n where 'n is some finite type. Now, is it possible to say that C is a subset of real^('n+'m) ? It seems that I can add types (theory Sum_Type), so I would imagine definition of direct sum as a function from (real^'n, real^'m) to real^('n+'m) such that first n coordinates of sum(x, y) coincides with x, and the next m coordinates - with y. Any ideas how to write down such a definition, which theories to look at, or may be suggestions how to formalize this in a different, more convenient way, would be appreciated.
Email Gateway (Aug 18 2022 at 15:25):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Montag, den 28.06.2010, 20:56 +0400 schrieb grechukbogdan:
Dear Isabelle Users
If A and B are sets, direct sum C of A and B is a set of pairs (a, b) where a \in A and b \in B.
My first question – is this direct sum defined somewhere in Isabelle?
This is defined in Isabelle/HOL as "A \<times> B" or "A <*>B" (in
ASCII).
Now, in my case A is a subset of R^n and B is a subset of R^m. In this case, clearly, C is a subset
of R^{n+m}. Currently, finite Cartesian product R^n formalized as type real^'n where 'n is some finite
type. Now, is it possible to say that C is a subset of real^('n+'m) ? It seems that I can add types
(theory Sum_Type), so I would imagine definition of direct sum as a function from (real^'n, real^'m)
to real^('n+'m) such that first n coordinates of sum(x, y) coincides with x, and the next m coordinates
- with y. Any ideas how to write down such a definition, which theories to look at, or may be suggestions
how to formalize this in a different, more convenient way, would be appreciated.
In the current _development_ version of Isabelle (unfortunately not in
Isabelle2009-2) real^'n is a euclidean space. When we add the type class
instantiation for products of euclidean spaces:
instantiation * :: (real_basis, real_basis) real_basis
...
instantiation * :: (euclidean_space, euclidean_space) euclidean_space
...
instantiation * :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
...
(with the appropriate definition for basis etc)
This should be a very convenient way as no isomorphisms need to be
specified to transfer between real^'n * real^'m and real^('n + 'm).
Everything including integration was updated to operate on euclidean
spaces.
This is already proved in Isabelle, I will push it tomorrow.
Greetings,
Johannes
Sincerely,
Bogdan Grechuk
Email Gateway (Aug 18 2022 at 15:37):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Johannes
I have download the last Development Snapshot from http://isabelle.in.tum.de/devel/
It is called Isabelle_01-Jul-2010.tar.gz
( By the way, website says that "version is built automatically every night from the repository sources." -- why the last version is July 1 not July 5th ?)
Are your changes included in this version already?
( I see new theory Cartesian_Euclidean_Space.thy, but I do not see something like
instantiation * :: (euclidean_space, euclidean_space) euclidean_space
)
If your changes are there, how exactly can I use this?
For example, what is now a correct formulation of the following lemma
Lemma: If A :: (real^'n set) is convex, and B :: (real^'m set) is convex, then A <*>B is a convex set in real^('n + 'm).
Will Isabelle automatically understand that if A :: (real^'n set) and B :: (real^'m set), then A <*>B lives in real^('n + 'm) ?
Sincerely,
Bogdan.
Email Gateway (Aug 18 2022 at 15:37):From: Johannes Hölzl <hoelzl@in.tum.de>
I don't know why the Isabelle snapshots are not updated, however when
you directly clone the mercurial repository
http://isabelle.in.tum.de/repos/isabelle
you get a version with the euclidean spaces.
Lemma: If A :: (real^'n set) is convex, and B :: (real^'m set) is
convex, then A <*>B is a convex set in real^('n + 'm).
Does not work, as real^'n * real^'m = real^('n + 'm), however you can
state:
lemma
fixes A :: "'a::euclidean_space set"
fixes B :: "'b::euclidean_space set"
assumes "convex A" and "convex B"
shows "convex (A <*> B)"
Of course now "A <*> B" is of type A * B, which is also in the
euclidean_space type class.
Probably you need to update you theories to use euclidean space instead
of real^'n. The changes are usual very easy, rewrite "x :: real^'n" to
"x :: 'n :: euclidean_space" (or ordered_euclidean_space)
\<chi> _ . _ -> \<chi>\<chi> _ . _ _ $ _ -> _ $$ _
The theorem names shouldn't be a problem. Sometimes you need to add the
assumption that a index is < DIM('a) as the indices are now more
selected from a finite type but just natural numbers.
Hope this helps!
Greetings,
Johannes
Email Gateway (Aug 18 2022 at 15:38):From: Makarius <makarius@sketis.net>
Because that build may fail, and even if it succeeds the result may be up
to surprises. Embarking on snapshots or raw repository versions means you
stop being a user and become an alpha/beta tester instead. Any problems
you encounter can be discussed on the isabelle-dev mailing list.
Makarius
Last updated: Apr 23 2024 at 12:29 UTC