====== 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

<code>
*** 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)
</code>

<code text 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
</code>