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

*To*: pvs-help@xxxxxxxxxxx*Subject*: Re: [PVS-Help] Min value in a set*From*: Jerome <jerome@xxxxxxxxxxxxxx>*Date*: Thu, 20 Mar 2008 16:12:09 -0700*In-reply-to*: <B91D26D8B493D8418EF309B13F90B326F921A1@NDMSEVS32B.ndc.nasa.gov>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <20080312000328.GB5840@cs.caltech.edu> <B91D26D8B493D8418EF309B13F90B326F921A1@NDMSEVS32B.ndc.nasa.gov>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-agent*: Mutt/1.4.1i

I'm having trouble expanding 'min' (over a set) within my proof. To illustrate, take the following theory: local: THEORY BEGIN natarray: TYPE = [posnat -> nat] indices: TYPE = finite_set[posnat] min_constant: LEMMA FORALL (J, K: indices): min(J) = min(K) END local When trying to prove 'min_constant', after skolemizing, I'd like to expand 'min', but I can't: {1} min(J!1) = min(K!1) Rule? (expand "min") No change on: (EXPAND "min") min_constant : |------- {1} min(J!1) = min(K!1) Why can't I perform the expansion? Even if I explicitly import 'finite_sets@finite_sets_minmax' in my theory, I get the same results. jerome On Wed, Mar 12, 2008 at 07:09:32AM -0500, Butler, Ricky W. (LARC-D320) wrote: >Jerome, > It distinguishes between them on the basis of the number of >arguments. Since both are in prelude, no IMPORTING statements are >needed. > >Note. See theory "finite_sets_minmax" in the "finite_sets" library for >a more general min/max over sets. > This can be located in the lib subdirectory of your installation >directory. It is imported as follows > > IMPORTING finite_sets@finite_sets_minmax > >The NASA libraries provide min and max over sets over a bounded domain. > > IMPORTING reals@bounded_reals > >See http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html >for information about how to install these. > >Rick > >> -----Original Message----- >> From: pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx >[mailto:pvs- >> help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx] On Behalf Of Jerome >> Sent: Tuesday, March 11, 2008 8:03 PM >> To: pvs-help@xxxxxxxxxxx >> Subject: [PVS-Help] Min value in a set >> >> I would like to use both 'min' operations in the prelude: min over a >> set and min of two values - how do I do it? In the former, I think the >> min found in 'min_nat' would do the trick, but I'm not sure how to >> access it. PVS always seems to think I want the min within 'real_defs' >> (which I do, for the latter). >> >> jerome >

- Prev by Date:
**RE: [PVS-Help] Min value in a set** - Next by Date:
**Re: [PVS-Help] Min value in a set** - Prev by thread:
**RE: [PVS-Help] Min value in a set** - Next by thread:
**Re: [PVS-Help] Min value in a set** - Index(es):