inst? and overloaded operators

[Pertti Kellomäki <pk@cs.tut.fi>]

Hi all,

I ran into the following problem in a proof. Consider the
following theories:

intval : DATATYPE
   BEGIN
     intval(v : int) : intval?
   END intval

intval_test : THEORY
BEGIN
   IMPORTING intval

    intval_peeling : lemma
     injective?(intval) =>
      forall (f : [[int,int] -> int]) :
        forall (i1, i2, i3, i4 : int) :
          intval(i1) = intval(i2) and intval(i3) = intval(i4)
          => intval(f(i1,i3)) = intval(f(i2,i4))

    intval_plus_peeling : lemma
     injective?(intval) =>
      forall (i1, i2, i3, i4 : int) :
        intval(i1) = intval(i2) and intval(i3) = intval(i4)
        => intval(i1+i3) = intval(i2+i4)
END intval_test

First the simple question: is there a direct way to
say in the datatype declaration that I want intval(X)=intval(Y)
to imply X=Y? It does not appear to be the case now.

My longer question concerns instantiation.
Clearly I can use intval_peeling as a lemma when proving
intval_plus_peeling. If I do instantiation by hand in the
proof, e.g. do (inst -1 "+" "i1!1" "i2!1" "i3!1" "i4!1"),
then everything works fine. However, if I let PVS do
instantiation with inst?, it produces two branches, one of
which is the unprovable subgoal

[-1]  injective?(intval)
[-2]  intval(i1!1) = intval(i2!1)
[-3]  intval(i3!1) = intval(i4!1)
   |-------
{1}   ((FORALL (x: numfield):
           real_pred(x) AND rational_pred(x) AND integer_pred(x))
         AND
         (FORALL (x: numfield):
            real_pred(x) AND rational_pred(x) AND integer_pred(x)))
        AND
        (FORALL (x1: [numfield, numfield]):
           real_pred(+(x1)) AND rational_pred(+(x1))
           AND integer_pred(+(x1)))
[2]   intval(i1!1 + i3!1) = intval(i2!1 + i4!1)

Is there a way around this or do I just have to instantiate
manually?

Thanks.
-- 
pertti