[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 =

  ftuple : LEMMA
,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

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


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

>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