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

[PVS-Help] inductive predicates

I’m trying to use an inductive predicate, and the corresponding induction scheme to proof some property, but encounter a series of problems.

First, the f2-example given in the PVS language report does not work. If I use the same definition as in this report:


f2(n,m:int)(x,y:int)(z:int): INDUCTIVE [int,int,int -> bool] =

LAMBDA (a,b,c:int): n = m IMPLIES f2(n,m)(x,y)(z)(a,b,c)


i get complaints from the system that this definition is incorrect. It seems as if PVS is rejecting the induction scheme it has generated. Actually, I was not able to define anything that had a predicate as a result, only 


f2(n,m:int)(x,y:int)(z:int) (a,b,c:int):: INDUCTIVE bool =

 n = m IMPLIES f2(n,m)(x,y)(z)(a,b,c)


seems to work.

The predicate I had in mind was something of this form (TYPES and CLT are recursive abstract DT)

                sem(t:TYPES): INDUCTIVE pred[CLT]


When I remove the predicate, e.g. by rewriting sem as follows

                sem(t:TYPES)(e:CLT): INDUCTIVE bool


i get something that is accepted, but the problem is that I don’t see how to instantiate the induction scheme such that the following lemma can be proven.


FORALL(t:TYPES, e:LC_DB): (FORALL(n:nat): sem(t)( FIX(n,e))) => sem(t)(e_fix(e))


FIX is a function producing a CLT, e_fix a constructor of CLT. Observe that the FORALL quantifier ends before the implication.


Can somebody help me?