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

Re: union variable binding operator



Mark Aronszajn (aronsz@csee.wvu.edu) writes:
> I'm pretty sure that PVS has a variable binding operator for unions (or
> a function from set&function pairs to sets), like there is for summing:
> 
> 	sum(S: set, f:[S -> int])
> 
> but I can't find it... Isn't there such a thing?
> 
> I.e. an operator 'union' so that where R is some set of sets
> 
> 				       |   |
> 	union(S: set, f: [S -> set]) = |   | f(x)
>                                        \___/
> 				  forall x in S
> 

  It is available in the finite_sets_sum theory of the finite sets
library that is distributed along with PVS:

  f,g: VAR [T -> R]
  S, A, B: VAR finite_set
  x: VAR T

  sum(S,f) : RECURSIVE R = 
    IF (empty?(S)) THEN zero
    ELSE f(choose(S)) + sum(rest(S),f)
    ENDIF MEASURE (LAMBDA S,f: card(S))

Rick Butler