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

[PVS-Help] Abtract datatypes: diffenrence between curried and uncurried map


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
 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_map.V1, Term_adt_map.F,


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,


Sjaak Smetsers