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

*To*: pvs@csl.sri.com*Subject*: inst? and overloaded operators*From*: Pertti Kellomäki <pk@cs.tut.fi>*Date*: Thu, 17 Apr 2003 15:26:48 +0300*Sender*: pvs-owner@csl.sri.com*User-Agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.1) Gecko/20021003

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

**Follow-Ups**:**Re: inst? and overloaded operators***From:*Hendrik Tews <tews@tcs.inf.tu-dresden.de>

- Prev by Date:
**No Subject** - Next by Date:
**Re: inst? and overloaded operators** - Prev by thread:
**New versions of Manip and Field strategies** - Next by thread:
**Re: inst? and overloaded operators** - Index(es):