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

[PVS-Help] Extending the prelude?

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