*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*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, 29 Jun 2010 22:37:09 +0200*In-reply-to*: <581661277744215@web145.yandex.ru>*Organization*: Technische Universität München*References*: <581661277744215@web145.yandex.ru>

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

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

- Previous by Date: Re: [isabelle] Type class instantiation without using Isar syntax
- Next by Date: [isabelle] const antiquotation
- Previous by Thread: Re: [isabelle] Can I define direct sum of sets in R^n and R^m
- Next by Thread: [isabelle] Code Generation: Error Messages
- Cl-isabelle-users June 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