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

Re: [PVS-Help] access n-th argument of a function?



Hi Romain,

Not sure if this helps, but in PVS there is no difference between a
function with n parameters and a function with 1 parameter that is an
n-tuple, e.g.,

f(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10:posreal) : posreal =
a1+a2+a3+a4+a5+a6+a7+a8+a9+a10

  ftuple : LEMMA
  FORALL 
(a:[posreal,posreal,posreal,posreal,posreal,posreal,posreal,posreal,posreal
,posreal]) :
   f(a) = a`1+a`2+a`3+a`4+a`5+a`6+a`7+a`8+a`9+a`10

Notice that in the lemma, the arguments are accessed through projections.


Unfortunately, it seems that the the projection has to be a numerical
constant. For example, the following definition is not syntactically
correct:

  
F(a:[posreal,posreal,posreal,posreal,posreal,posreal,posreal,posreal,posrea
l,posreal])(n:subrange(1,10)) : posreal = f(a`n)

It seems that to define F you still need to do something like

    IF n = 1 THEN a`1
    ELSIF n = 2 THEN a`2
    ...
    ENDIF




Cesar

On 4/25/14 4:06 PM, "Romain Jobredeaux" <romain.jobredeaux@xxxxxxxxxx>
wrote:

>Hello,
>
>I am curious if there is in the PVS syntax, a way to access the n-th
>argument of a function by its index, something like
>
>F(a1,a2,a3,a4,a5,a6,... : posnat) :posnat  = args(3)
>
>where args(3) would be a3.
>
>what I am actually trying to do is to convert a function with a big
>number of arguments into a map:
>
>F(a1,a2,a3,a4:posnat) = lambda ( i : below(n) ) : if i=1 then a1 else if
>i=2 then a2 else if i=3 then a3....
>
>but it seems very impractical using if-functions.
>
>Thanks in advance,
>
>Romain Jobredeaux
>
>
>  
>