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

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