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

Re: [PVS-Help] Extending the prelude?



Hi Cesar,

My reasoning is that it would be great to have access to these lemmas without having to use an IMPORTING statement in the theory before beginning the proof. If I insert this lemma into the theory reals@abs_lems, then I would have to have “IMPORTING reals@abs_lems” in the body of my theory, correct?

Thanks a lot for directing me to Section 2.4. That does seem like it will do the trick.

Best Regards,
-Ben

> On Jul 9, 2015, at 12:37 AM, MUNOZ, CESAR (LARC-D320) <cesar.a.munoz@xxxxxxxx> wrote:
> 
> 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
>> 
>> 
>> 
>> 
>> 
>> 
>> 
>