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

Re: [PVS-Help] R_pred



Thanks everybody - things make sense now.

Natarajan Shankar wrote:
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