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

Re: [PVS-Help] Functions in record types



Hi Hanne,

It's actually cat2b that has the definition, not comp.  If you just
(expand "cat3" -5), it should then be beta-reducible to the form you
want.

Regards,
Sam

Hanne Gottliebsen <hago@dcs.qmul.ac.uk> wrote:

> Date: Fri, 14 Jul 2006 18:43:29 +0100
> From: Hanne Gottliebsen <hago@dcs.qmul.ac.uk>
> Organization: Department of Computer Science, QMUL
> To: pvs-help@csl.sri.com
> X-DCS-Auth-User: hago
> Subject: [PVS-Help] Functions in record types
> Sender: pvs-help-bounces+owre=csl.sri.com@csl.sri.com
> 
> I have a record type where some of the components are functions, for
> example:
> 
>   cat2b : cat_TYPE = (# C0 := { x | x = 1 OR x = 2},
>                         C1 := { x | x = 3 OR x = 4},
>                         s := LAMBDA x :
>                             IF (x = 3 OR x = 4) THEN x-2 ELSE x ENDIF,
>                         t := LAMBDA x :
>                             IF (x = 3 OR x = 4) THEN x-2 ELSE x ENDIF,
>                         I := LAMBDA x :
>                             IF (x = 1 OR x = 2) THEN x+2 ELSE x ENDIF,
>                         comp := LAMBDA x,y : x #)
> 
> 
> In a proof I would like to be able to evaluate those functions on certain
> arguments. For example in the following, I would like to expand (or
> similar) comp:
> 
> 
> {-1}  cat3`C1(f!1)
> {-2}  cat3`C1(g!1)
> {-3}  cat3`C1(h!1)
> [-4]  (cat3`s(f!1) = cat3`t(g!1))
> [-5]  h!1 = cat3`comp(f!1, g!1)
>    |-------
> [1]   (cat3`s(h!1) = cat3`s(f!1) AND
>          cat3`t(h!1) = cat3`t(g!1) AND cat3`t(f!1) = cat3`s(g!1))
>