[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?

 

Sjaak