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

*To*: <pvs-help@xxxxxxxxxxx>*Subject*: [PVS-Help] Abtract datatypes: diffenrence between curried and uncurried map*From*: <S.Smetsers@xxxxxxxx>*Date*: Fri, 21 Dec 2012 09:03:21 +0100*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://mls.csl.sri.com/cgi-bin/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://mls.csl.sri.com/cgi-bin/mailman/options/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*Thread-index*: Ac3fT8kqT4PUYKaJSVq6Jf8A/XM7iQ==

Hi, I have the following abstract data type: == Term[ V : TYPE, % for variables F : TYPE, % for operations ar : [F -> nat] % for arity of operations

tvar(var_id:V) :tvar? tapp(op:F, args:[below(ar(op)) -> Term]) : tapp? END Term == And I'm trying to define the following composition property about map (that I've copied form the prelude where it was given for lists and sequences) == T_map_props [F : TYPE, ar : [F -> nat], T1, T2, T3: TYPE]: THEORY BEGIN IMPORTING Term f1: VAR [T1 -> T2] f2: VAR [T2 -> T3] t: VAR Term[T1,F,ar] map_T_composition: LEMMA map(f2)(map(f1)(t)) = map(f2 o f1)(t) END T_map_props == This definition will not compile; it produces the error: == Could not determine the full theory instance for = Theory instance: equalities [Term_adt [Term_adt_map.V1, Term_adt_map.F, Term_adt_map.ar].Term] == If I use the uncurried map : == map_T_composition: LEMMA map(f2,map(f1,t)) = map(f2 o f1,t) == Pvs is satisfied. What's the difference? What do i have to do to get the first version accepted? I've tried almost anything I could think of (in terms of imports, or qualified names), but nothing seems to work . Actually I would prefer the following version == map_T_composition: LEMMA (map(f2) o map(f1))(t) = map(f2 o f1,t) == which doesn't work either, Thanks, Sjaak Smetsers

- Prev by Date:
**Re: [PVS-Help] Abtract datatypes in abstract data types** - Next by Date:
**Re: [PVS-Help] How to continue this proof?** - Previous by thread:
**[PVS-Help] Abtract datatypes in abstract data types** - Next by thread:
**[PVS-Help] PVS theory for C strings?** - Index(es):