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

*To*: pvs-help@csl.sri.com*Subject*: Union over a set; quantifiers*From*: polak <indra@cs.rug.nl>*Date*: Mon, 06 Oct 1997 13:56:47 +0200*Sender*: indra@rug103.cs.rug.nl

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

- Prev by Date:
**Re: WITH and dependent types** - Next by Date:
**How can I prove this?** - Prev by thread:
**How can I prove this?** - Next by thread:
**Accumulation quantifier support?** - Index(es):