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

[PVS-Help] Functions in record types



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))

However, on (expand "cat3`comp") PVS complains that the ` is garbage.


Shouldn't I be able to expand this function? And if not, does anyone 
have any hints as to how I can change my definition to be more workable 
in PVS?


Thanks,
Hanne
-- 
---------------------------------------------------------
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
---------------------------------------------------------