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

Union over a set; quantifiers

Dear PVS users,

I would like to formalize a quantifier like "union over a set" in PVS.
I was wondering whether this has done before by someone.

So in formal notation:

(Ux : p(x) : q(x)) = the union of all terms of the form q(x) which
satisfy p(x).

I can define something like that in terms of a lambda term and an
exists, say

U(f : [X -> [bool, X]]) : setof[X] =

  { x : X | proj_1(f(x)) AND 
            (EXISTS (y : X): y = proj_2(f(x))) }

Then I get expressions like 
U(lambda (x:X): (p(x),q(x)))
in which a lambda is visible, and when reasoning with the quantifier one 
has to reason about exists which is awkward in most cases.

One solution is ofcourse to create an interface (frontend) for PVS in
which expressions like 
(Ux : p(x) : q(x)) are automatically transformed to the above syntax,
but in proofs the translation in the other direction is also necessary
and I do not see how to do this automatically in an easy way.

If it was possible to define new quantifiers in PVS, then I would be 
happy, but I do not know how to do that. Another thing is that one would 
like to have a polymorphic quantifier, because in the above example, 
if one has defined the constant U in a theory with type parameter X, 
one has to do an import for every instance one is interested in, and
one must sometimes disambiguate the different constants U in order to 
type-check. This is all very inconvenient for something as elementary 
as a union over a set.

Any help would be very much appreciated.

With kind regards, 


Indra Polak
email: indra@cs.rug.nl