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

[PVS-Help] singleton lists

Hi, I'm having I'm having trouble working with an antecedent:

{-10} cons(c0`next(car(c0`list)), null) = (: empty :)

I'd like to simplify this to

c0`next(car(c0`list)) = empty

('empty' is a data constructor constant)

I can't get PVS to recognise that the LHS of -10 can be simplified
down.  Is there some property I can use?  (I can't figure out
exactly what list_rep does in the prelude.) If so, would PVS then
work out that equality on singleton lists is equivalent to equality
on their elements?

Now a couple of related questions:

In trying to solve the above problem I proved the lemma:

	cons_null: THEOREM
			(forall f, x: (: x :) = cons(x, null))

When I tried introducing this using 'lemma', PVS seemed to automatically
simplify it to true, ie, I didn't get any addition to the antecedents
by using the lemma rule (with appropriate substitutions).

You'll note the inclusion of the unused
variable 'f' in the definition of 'cons_null'.  Theorems apparently
need two variables for the 'lemma' command to work.  Is this
correct, and if so is there a neater work around?