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

*To*: pvs-help@csl.sri.com*Subject*: Re: union variable binding operator*From*: "Ricky W. Butler" <r.w.butler@larc.larc.nasa.gov>*Date*: Mon, 27 Sep 1999 06:46:35 -0400 (EDT)*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <Pine.GSO.4.10.9909241645200.27169-100000@naur.csee.wvu.edu>*References*: <Pine.GSO.4.10.9909241645200.27169-100000@naur.csee.wvu.edu>*Reply-To*: R.W.Butler@larc.nasa.gov

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

**References**:**union variable binding operator***From:*Mark Aronszajn <aronsz@csee.wvu.edu>

- Prev by Date:
**sorry, slight slip in my query** - Next by Date:
**Moving existential quantifiers out over universal quantifiers** - Prev by thread:
**union variable binding operator** - Next by thread:
**using grind** - Index(es):