Re: [PVS-Help] Functions in record types

[Hanne Gottliebsen <hago@dcs.qmul.ac.uk>]

Hi Sam,

Thanks, that was just what I needed (of course, me definition was still 
wrong...).


Hanne



Sam Owre wrote:
> 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))
>>


-- 
---------------------------------------------------------
Dr. Hanne Gottliebsen    Department of Computer Science
hago@dcs.qmul.ac.uk      Queen Mary, University of London
Ph: +44 (0) 207 882 5259
   - I want a single-skin cotton tent like Mr Weasley's
---------------------------------------------------------