# Re: [PVS-Help] Body of lemmas

```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)))
sin_2a is an instance of #<standard-class name-expr>:

The following slots have :instance allocation:
place              nil
pvs-sxhash-value   nil
parens             0
type               nil
free-variables     unbound
free-parameters    unbound
mod-id             nil
library            nil
actuals            nil
id                 sin_2a
mappings           nil
target             nil
resolutions        (#<Resolution trig_basic.sin_2a:formula>)

If you drill down, you'll find you can get what you want as follows:

Rule? (lisp (show (definition (declaration (car (resolutions
(formula-resolutions 'sin_2a)))))))

sin(2 * a) = 2 * sin(a) * cos(a) is an instance of
#<standard-class infix-equation>:
The following slots have :instance allocation:
place              #(93 22 93 52)
pvs-sxhash-value   nil
parens             0
type               boolean
free-variables     (a)
free-parameters    unbound
operator           =
argument           (sin(2 * a), 2 * sin(a) * cos(a))

sin(2 * a) = 2 * sin(a) * cos(a)

>From there you can dig down deeper if necessary to access interior PVS
expression objects.  All of this is doable within strategies; just call the
Lisp functions as needed.

Regards,

Ben Di Vito
1 South Wright Street, MS 130
NASA Langley Research Center
Hampton, VA 23681   USA

voice: +1-757-864-4883     fax: +1-757-864-4234
b.divito@nasa.gov
http://shemesh.larc.nasa.gov/people/bld

```