[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Mathematical and PVS syntactic equivalence?



Hello,

Giving a set of reals S, I am trying to specify a + operation which
constructs another set being the same as S except that every member has
been added a fixed constant:

In PVS I wrote:

  REALSET: TYPE = setof[real]
  ; + (I: REALSET, delta: real): REALSET =
    {t:real | EXISTS(i: real): member(i, I) AND t = i + delta}


Mathematically speaking I would rather write something like:

  ; + (I: REALSET, delta: real): REALSET =
    {i + delta | member(i, I)}

(By the way, are the two specifications equivalent?)

I am wondering if it is possible to specify the + operation in a way
which would be syntactically (and maybe semantically) closer to the
mathematical one...

Thank you for your help...
-- 

    - François

      (((((
    g( o - )g
 -oOO--(_)--OOo-------------------------------------------------------
|              François Chabot                  Voice: +32-71-259-430 |
|              CEDITI - FUNDP                     Fax: +32-71-372-064 |
|              Avenue Georges Lemaître, 21   email: fch@fun.cediti.be |
|  .ooo0       6041 Gosselies          http://www.fun.cediti.be/~fch/ |
|  (   ) 0ooo. Belgium                                                |
 ---\ (--(   )--------------------------------------------------------
     \_)  ) /
         (_/