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

[PVS-Help] Deferring TCCs



Hi, is there a way of deferring TCCs generated from definitions to
being checked where the definitions are used in a theorem?
For instance, consider the following theory:

first_one: THEORY BEGIN
	l: VAR list[nat]
	first_one(l): bool = car(l) = 1
END first_one

It generates one TCC:

first_one_TCC1: OBLIGATION FORALL (l: list[nat]): cons?[nat](l);

This can apparently never be satisfied, ie, every proof that
depends on first_one will only ever be "proved - incomplete".
However I can be careful with my use of first_one such that any time
it is used in a theorem its actual parameter will satisfy the TCC
(ie. is non-null).  (In fact, it seems to me that I would not be
able to prove anything useful using first_one if the parameter is
nonempty since 'car' is meaningless in this case.)

Is there a general workaround that scales for many theorems like
first_one with possibly non-trivial TCCs?  

One option is to add "cons?(l) and" to the definition, but this is
redundant if I know first_one will only be used in a context where
cons?(l) is satisfied, and in general the approach can clutter
the definitions if the conditions required to avoid generating 
TCCs are nontrivial.  Perhaps there is another way of dealing with
the situation, along the lines of using judgements.

What I'd like to see is first_one generate a TCC 'flag', as above.
Then consider a theorem which uses first_one, eg,

th: THEORY BEGIN
	importing first_one
	l: VAR list[nat]
	x: THEOREM
		(forall l: l = (: 1 :) implies first_one(l))
END th

The theorem generates the TCC 
	(forall l: l = (: 1 :) implies cons?(l))

Can this sort of behaviour be achieved in PVS?  Or is there some
reason why it is a bad idea?  

Rob