Re: [PVS-Help] R_pred

[Natarajan Shankar <shankar@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