Short PVS manual
Wim H. Hesselink, September 2004 (version September 2009)

Only an introductory sketch. See the online manuals for more.

To call PVS in the shell: call
pvs &
This gives an emacs-window for PVS. For the text editor emacs, see its
tutorials.

In emacs you can open a declaration file in the usual way:
Cx Cf filename.pvs
loads a file with a theory or theories, or opens a new one. 

Edit this file in the usual way until you think it ready. 
Then save and check syntax and types by
Cc Ct
This reports syntax or typing errors, if any. If not you can proceed.

Consult the PVS menu for:
1. which results have been proved in the theory (once you have proved things)
2. to consult the prelude file
3. to edit a previous proof (advanced)
4. to call the prover, see however below. 

CALLING AND USING THE PROVER

If you want to prove some lemma or theorem, place the cursor in it and:
Cc Cp x
This splits the window, creates a buffer *pvs* with a LISP reader, and an 
X-window where a proof tree can grow. 
The prompt of the LISP reader is "Rule? ".

Now there are numerous proof commands available. These are in two forms:
1. LISP-like S-expressions, to be typed after "Rule?"
2. Emacs shortcuts, usually starting with "tab"
NB The declaration-file and the expression language are case-sensitive, 
but the LISP-reader is not, apart from the expressions between double quotes.

(quit)     or   tab Cq   exit the prover (quit without parentheses also works)
(undo)     or   tab u    undo latest prover command
(postpone) or   tab P    go to the next open leaf of the current proof tree

(flatten)  or   tab f    simplify the sequent by removing AND from antecent,
                         and OR and IMPLIES from consequent, and NOT from both
(split)    or   tab s    split the sequent by eliminating OR and IMPLIES 
                         from antecedent, and AND from consequent;
                         you can give it a line number
(assert)   or   tab a    for equational reasoning (never splits current goal)
(prop)     or   tab p    all propositional reasoning (may split current goal)
Because (split) and (prop) split the sequent, they can create extra work by 
letting you give the same argument several times. 

(beta)     or   tab b    beta reduction of LAMBDA applications (also LET)
(lift-if)  or   tab l    move embedded IFs outward
(iff)      or   tab F    replace boolean equality by IFF
(grind)    or   tab G    reason as far as possible (use only when conclusive)

If (grind) does not stop within a reasonable time, you can force
termination by the command CcCc (controle C twice). This gives you a
question from the Lisp reader how to proceed. You can answer this usually 
with ":continue 1". 

(skolem!)  or   tab !    creates a fresh free "skolem" variable for EXISTS
                         in antecedent or FORALL in consequent
(skosimp)  or   tab S    <return> or line number(s) in minibuffer
                         this is skolem! with flattening
(skosimp*) or   tab *    repeated application of (skosimp)
(induct "identifier")    induction, if identifier is of type "nat"

Instantiation of FORALL in antecedent or EXISTS in consequent:
(inst-cp <line> "expression")   instantiate with expression, do not hide
(inst <line> "expression")      instantiate with expression, and hide
(inst?)    or   tab ?           also tries to find suitable instantiation

(expand "identifier")  or  tab e with cursor on the identifier
                                expand the definition of the identifier
(expand "identifier" <lines>)   expand the identifier only in <lines>

tab E is (apply-extensionality :hide t)  equality of functions or structures

(case "boolean expression")         for case splitting 
(name "identifier" "expression")    to introduce a name for an expression 

Replacing for equational reasoning:
(replace <lineA>)              
if the line <lineA> is an equality X = Y, replace all occurrences of X by Y
(replace <lineA> <lines>)   similar, restricted to <lines>
(replace <lineA> * rl)      similar, but replace Y by X
If <lineA> in antecedent or consequent is not an equality but a formula F, 
do as if it were "F = true" or "F = false", respectively. 

Adding subtype information:
(typepred "expression") gives the type predicate of the expression.
Shortcut: tab t, asks for the expression in minibuffer.

Hiding, deletion, and copying of formulas
(hide <lines>)             hide the <lines>
They can be reobtained by first typing Mx show-hidden-formulas.
Then use prover command (reveal <lines>).
(delete <lines>)           destructive deletion, but for (undo).
(hide-all-but (<lines>))   hide everything apart from <lines>, 
                           note parentheses!
(copy <lineA>)             make additional copy of <lineA>

If "lemmaA" is a reachable lemma, it can be invoked by 
(lemma "lemmaA")           adds the lemma as a new antecedent

I prefer to apply "use" and let PVS find suitable instantiations:
(use "lemma")              tries an obvious instantiation for all free 
                           variables in "lemma"
(use "lemma" ("x" "ex" "y" "ey"))   
         instantiates "x" with expression "ex" and "y" with "ey" in "lemma" 
         and tries to instantiate the other free variables suitably.

If you want to undo a partial prover command, try: 
Cg (as usual in emacs).

Note that any line that starts with Rule? can be used to give a prover command.
So it is often convenient to edit a previous prover command and then <return> 
on that line. This is especially useful if the prover command is complicated.
In emacs, you can search back and forth in the LISP-window by Cr and Cs.

Other ways to call the prover from a declaration:
Cc Cp t:  (re)prove all lemmas in the theory with the current proofs
Cc Cp i:  (re)prove all lemmas in the import chain with the current proofs
Cc Cq s:  show TCCs (type correctness conditions)
          Here you can also call Cc Cp x to prove a TCC.