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

*To*: Jerome <jerome@xxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] R_pred*From*: Natarajan Shankar <shankar@xxxxxxxxxxx>*Date*: Fri, 07 Nov 2008 15:08:09 -0800*Cc*: PVS Help <pvs-help@xxxxxxxxxxx>*Comments*: In-reply-to Jerome <jerome@cs.caltech.edu> message dated "Fri, 07 Nov 2008 12:55:25 -0800."*In-reply-to*: <20081107205525.GD3397@cs.caltech.edu>*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*: <20081106233402.GA16079@cs.caltech.edu> <49144822.5010608@nianet.org> <20081107205525.GD3397@cs.caltech.edu>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Jerome: When you have a theory parameter given as R: TYPE FROM nnreal a subtype predicate R_pred is automatically generated so that R = {s : nnreal | R_pred(s)}. Now, when you add two expressions a and b of type R and want the result a+b to be of type R, you need to show that R_pred(a) and R_pred(b) => R_pred(a+b). One way to avoid this problem is to just use nnreal in place of R. The other option is to add an assumption about R in the ASSUMING section that R is closed under addition. -Shankar Jerome <jerome@xxxxxxxxxxxxxx> wrote: > R: TYPE FROM nnreal > > Within the theory, distance and W are functions from some type to R: > > distance: [D -> R] > W: [D, D -> R] > > Thus, to discharge [1] do I need to show that the addition of two > non-negative real numbers is still a non-negative real number? My > original question stems more from surprise (and lazyness) that this > wasn't taken care of by some prelude magic :) > > Is this what [1] wants me to show? And, in general, how do I interpret > the _pred convention? Thanks > > jerome

- Prev by Date:
**Re: [PVS-Help] R_pred** - Next by Date:
**Re: [PVS-Help] R_pred** - Prev by thread:
**Re: [PVS-Help] R_pred** - Next by thread:
**Re: [PVS-Help] R_pred** - Index(es):