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

Re: [PVS-Help] 'divides' definition



R. Colvin wrote:
> How can I use 'use' or 'lemma' to introduce an instance of the
> 'divides' definition from theory divides in the prelude?  I've tried 
> 
> (lemma divides (n "L" m "L")) and
> (lemma divides (n "L")) 
> and some others and was given the message:
> 
> 	"Found 2 resolutions for divides relative to the substitution.
> 	Please check substitution, provide actual parameters for lemma
> 	name, or supply more substitutions."
> 
> Thanks,
> Rob
> 

It looks like there is no way to disambiguate between
the two possible instances. There are two definitions
of divides. Both come from the same theory and have
the same parameters.

On the other hand, it's not clear why you're trying
to introduce an instance of the divides definition,
via the "lemma" command. (expand or rewrite are typically
more useful for definitions). If what you need is
"divides(L,L)" as an antecedent, try using
(lemma "devides_reflexive" ("n" "L")).

If you absolutely need to introduce the definition
of "divides", then a simple way to do it is to use

(case "divides(L, L) = EXISTS (n: nat): L = L * n")

and then discharge the subgoal via (expand "divides").

Bruno