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

sorry, slight slip in my query



Sorry, there was a slight slip in my last PVS query. Here's the question
again, corrected:

Does PVS have a variable binding operator for unions (or a function from
set & function pairs to sets), like the one for summation?

I've looked in the Prelude and in the finite_sets library, and haven't
seen it... Isn't there such a thing?

I.e. an operator 'union' so that where S is a set, and f is a function
mapping each element of S to an element in some set of sets, R, we have

				     |  |
    union(S: set, f: [S -> R])   =   |  | f(x)
                                     \__/
				  forall x in S

I thought PVS came with this operation pre-defined.  Thanks, sorry if I'm
missing something obvious...

Mark Aronszajn