*Subject*: Re: [isabelle] Can I define direct sum of sets in R^n and R^m*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Tue, 06 Jul 2010 16:49:47 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <28571278427014@web133.yandex.ru>*Organization*: Technische Universität München*References*: <581661277744215@web145.yandex.ru> <1277843829.2006.7112.camel@macbroy12.informatik.tu-muenchen.de> <28571278427014@web133.yandex.ru>

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 Am Dienstag, den 06.07.2010, 18:36 +0400 schrieb grechukbogdan: > 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

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

- Previous by Date: Re: [isabelle] Can I define direct sum of sets in R^n and R^m
- Next by Date: [isabelle] Attributes for unnamed facts in obtains
- Previous by Thread: Re: [isabelle] Can I define direct sum of sets in R^n and R^m
- 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