Proveit Batch Utility

proveit is a command line utility for running the theorem prover in batch mode.

$ proveit --importchain --clean use_bag.pvs

This example can be used to test proveit and the installation of NASA PVS library.

Example

Download the file below as use_bag.pvs (uses the NASA Library for Bag)
All the conjectures can be proved with (grind)
execute the above proveit command in the terminal
This will generate use_bag.summary

*** use_bag (17:18:33 8/25/2016)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
*** Trusted Oracles
***   MetiTarski: MetiTarski Theorem Prover via PVS proof rule metit
*** 
 Proof summary for theory use_bag
    test1.................................proved - complete   [shostak](0.04 s)
    test2.................................proved - complete   [shostak](0.03 s)
    test3.................................proved - complete   [shostak](0.01 s)
    test4.................................proved - complete   [shostak](0.01 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.09 s)

Grand Totals: 4 proofs, 4 attempted, 4 succeeded (0.09 s)

use_bag

use_bag : THEORY
BEGIN
  IMPORTING structures@bags
  % NASA library
 
% All the conjectures prove with grind
  test1: CONJECTURE
    member(5,insert(5,emptybag)) = 1
 
%|- test1 : PROOF
%|- (grind)
%|- QED
 
  test2: CONJECTURE
        count(1, emptybag) = 0 
    AND count(1, insert(1, emptybag)) = 1
    AND count(1, insert(1, insert(1, emptybag))) = 2
 
%|- test2 : PROOF
%|- (grind)
%|- QED
 
  PRODUCT: TYPE = posnat
  prd, prd1, prd2: VAR PRODUCT
 
  SET_PRODUCT: TYPE = setof[PRODUCT]
  sp, sp1, sp2: VAR SET_PRODUCT
 
   % add product p to set of products sp
  add_type(p:PRODUCT,sp): SET_PRODUCT = 
    union(singleton(p), sp)
 
  %IMPORTING structures@bags[PRODUCT]
  STOCK: TYPE = bag[PRODUCT]
  st, st1, st2: VAR STOCK
 
  add_product(st1, st): STOCK = % add st1 to stock st if dom(st1)
    plus(st1, st)
 
  p1,p2,p3: PRODUCT
 
  test3: CONJECTURE
    st = emptybag WITH [p1 := 1, p2 := 2] implies count(p2, st) = 2
 
%|- test3 : PROOF
%|- (grind)
%|- QED
 
  cart1: bag[PRODUCT] = emptybag WITH [p1 := 1, p2 := 2]
 
  %insert(x,b): bag = (LAMBDA t: IF x = t THEN b(t) + 1 ELSE b(t) ENDIF)
  test4: CONJECTURE
    p3 /= p2 AND p2 /= p1 AND p1 /= p3 => count(p3, cart1) = 0
 
%|- test4 : PROOF
%|- (grind)
%|- QED
 
END use_bag