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

Re: [PVS-Help] Body of lemmas



On Thu, Jun 23, 2005 at 02:01:04PM -0400, Ben Di Vito wrote:
> On Thursday 23 June 2005 12:24, Erika Rice wrote:
> > Is it possible to access the body of a particlar lemma from a
> > strategy?  My goal is to write a strategy where I can invoke
> > (strategy "lemma") in a manner similar to (rewrite "lemma").
> 
> Yes, this is possible.  Suppose you have the following lemma:
> 
>    sin_2a     : LEMMA sin(2*a) = 2 * sin(a) * cos(a)
> 
> PVS has the lookup function 'formula-resolutions' that returns a
> name-expr 
> object for a given name.  You can use show or describe to look at
> the 
> structure of this object:
> 
> Rule? (lisp (show (formula-resolutions 'sin_2a)))

When I  try 
    Rule? (lisp (show (formula-resolutions 'mylemma)))
I get the error
    Error: No methods applicable for generic function
           #<standard-generic-function actuals> with args
           (mylemma) of classes (symbol)
      [condition type: program-error]

I am using PVS 3.2.  Any enlightenment would be appreciated.

        Erika