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

*To*: <pvs-help@xxxxxxxxxxx>*Subject*: [PVS-Help] inductive predicates*From*: "Sjaak Smetsers" <s.smetsers@xxxxxxxxxxxxx>*Date*: Wed, 6 Oct 2010 15:32:29 +0200*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*Thread-Index*: ActlVcfbt10KxFmORqSbd3wY/yNaWw==

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 |

- Prev by Date:
**Re: [PVS-Help] Problems with CMU Lisp version of PVS 4.2** - Next by Date:
**[PVS-Help] PVS logical engine** - Prev by thread:
**[PVS-Help] PVS logical engine** - Next by thread:
**[PVS-Help] Problems with CMU Lisp version of PVS 4.2** - Index(es):