[PVS-Help] repeat depending in datatype

[qgxu <qgxu@mail.shu.edu.cn>]

Hello everyone:

the following is a "toy" theory written in PVS 3.2 with patch.

redep: THEORY
BEGIN
neq(i: nat): TYPE = {x: nat | x /= i}
c1(i: nat, j: neq(i))(x: int): bool =
COND i = 0 -> x <= 0, j = 0 -> x >= 0, ELSE -> TRUE ENDCOND

DTP: DATATYPE
BEGIN
fun(i: nat, j: neq(i), k: (c1(i, j))): fun?
END DTP

END redep

In the DTP specification, the type of k is depent on i and j, but the
following unproved tcc is generated.

% Subtype TCC generated for j(d)
% expected type neq(i)
j_TCC1: OBLIGATION FORALL (d: DTP, i: nat): j(d) /= i;

why the PVS typechecker cannot identify the last j in fun is of type neq(i)?

if fun(i: nat, j: neq(i), k: (c1(i, j))) is defined as a function. this
tcc is not genereated.
if k is depent on i , this tcc doesn't also generate.

why?

Thanks in advance.


Q.G., XU
21/12/2005