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



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.