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

Re: [PVS-Help] Extending the prelude?



Ben, 
The short answer is yes (see page 20, Section 2.4, of our tutorial in
http://shemesh.larc.nasa.gov/people/cam/publications/NASA-CP-2003-212448.pd
f). Proveit supports this type of extensions.

The short question is why? There is a theory reals@abs_lems in the NAS PVS
Library, where your lemma is welcome. From there, you can easily import
that theory and set an auto-rewrite. Let me know if this option works for
you and add the lemma there.

Cesar
-- 
Cesar A. Munoz                             NASA Langley Research Center
Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234




On 7/7/15 9:35 PM, "pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx on
behalf of Ben Hocking"
<pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx on behalf of
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

>Is there a way to “extend” prelude.pvs? For example, if I want to make
>the following proven lemma available to proofs in any theory without
>requiring them to have an IMPORTING statement for the helper lemma:
>
>
>  abs_bounding:
>
>LEMMA             
>    
>FORALL(a: real, nnx: nnreal, b: real, nny: nnreal):
>      abs(a)
>
><= nnx 
>AND abs(b) 
><= nny 
>IMPLIES          
>        
>-(nnx 
>* nny) 
><= (a 
>* b) 
>AND               
>         (a
>
>* b)     
><= (nnx 
>* nny);           
>
>
>
>Is there a way to do this? I’ve tried renaming the containing file
>prelude.pvs (in the current working directory), but that did not do the
>job.
>
>
>Best Regards,
>Ben Hocking
>ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>
>
>
>
>
>
>