%% Examples of use of ProofLite 6.0
%% Cesar Munoz 
%% http://shemesh.larc.nasa.gov/fm/pvs/ProofLite
%% NASA LaRC

prooflite_examples : THEORY
BEGIN

% INSTRUCTIONS (Interactive Mode)
% - Typecheck this file and use the command 
%   M-x load-prelude-library ProofLite
%
% - To install all the ProofLite scripts type
%   M-x install-prooflite-scripts-theory (C-c it)
%
% - To install a particular ProofLite script, place the cursor on the script
%   and type 
%   M-x install-prooflite-script (C-c ip)
%
% CAVEATS: 
% By default proofs are not overridden. To force overriding use the commands:
% - M-x install-prooflite-scripts-theory! (C-c !t)
% - M-x install-prooflite-script! (C-c !p)
% 
% INSTRUCTIONS (Batch Mode)
%
% Run the proveit utility: 
% <pvs-dir>/proveit prooflite_examples
%

  a,b : VAR real
  nza : VAR nzreal

  l1: LEMMA
    a*a >= 0
  % One line proof scripts
  %|- l1 : PROOF (grind) QED

  l2: LEMMA
    (nza/2)*(2/nza) = 1
  % Multiple line proof scripts
  %|- l2 : PROOF 
  %|-   (then (skosimp)
  %|-         (grind)) 
  %|- QED

  l3: LEMMA
    a*a >= 0

  l4: LEMMA
    (nza/2)*(2/nza) = 1

  % Sharing proof scripts
  %|- l3 : PROOF 
  %|- l4 : PROOF 
  %|-   (grind)
  %|- QED

  l3a: LEMMA
    a*a >= 0

  l4a: LEMMA
    (nza/2)*(2/nza) = 1

  % Proof scripts for name-matching lemmas
  %|- l*a : PROOF 
  %|-   (grind)
  %|- QED

  l_5_6 : LEMMA
    EXISTS (a) :  5 < a AND a < 6

  l_6_7 : LEMMA
    EXISTS (a) :  6 < a AND a < 7

  % Proof macros
  %|- l_*_* : PROOF 
  %|-   (then (skip-msg "Proving Lemma: $0") 
  %|-         (inst 1 "$1 + ($2 - $1)/2")
  %|-         (grind))  
  %|- QED     

  l_8 : LEMMA
    EXISTS (a,b) :  a+b = 8

  l_9 : LEMMA
    EXISTS (a,b) :  a+b = 9 

  % Parametric proofs 
  %|- l_8[2;6] : PROOF 
  %|- l_9[4;5] : PROOF
  %|-   (then (skip-msg "Proving Lemma: $0") 
  %|-         (inst 1 "#1" "#2")
  %|-         (grind))  
  %|- QED     

END prooflite_examples