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?