*To*: Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] Can I define direct sum of sets in R^n and R^m*From*: grechukbogdan <grechukbogdan at yandex.ru>*Date*: Tue, 06 Jul 2010 18:36:53 +0400*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1277843829.2006.7112.camel@macbroy12.informatik.tu-muenchen.de>*References*: <581661277744215@web145.yandex.ru> <1277843829.2006.7112.camel@macbroy12.informatik.tu-muenchen.de>

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. 30.06.10, 00:37, "Johannes Hölzl" <hoelzl at 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 \ 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 > > > > > > -- Яндекс.Почта. Письма есть. Спама - нет. http://mail.yandex.ru/nospam/sign

**Follow-Ups**:**Re: [isabelle] Can I define direct sum of sets in R^n and R^m***From:*Johannes Hölzl

**Re: [isabelle] Can I define direct sum of sets in R^n and R^m***From:*Makarius

- Previous by Date: [isabelle] VSTTE 2010: First Call for Participation
- Next by Date: Re: [isabelle] Can I define direct sum of sets in R^n and R^m
- Previous by Thread: [isabelle] VSTTE 2010: First Call for Participation
- Next by Thread: Re: [isabelle] Can I define direct sum of sets in R^n and R^m
- Cl-isabelle-users July 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list