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