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



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








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