# Re: PVS Problem

```Dear Galina,

1.  The commands to automatically apply a specified prover strategy
(grind, by default) to all the theorems in a theory or file are

prove-untried-theory, prut (C-c C-p u) Try untried proofs with given strategy
prove-untried-pvs-file, pruf (C-c C-p U) Try untried proofs with given strategy

I cut and pasted these lines from the PVS help file.  There's
additional description in the relevant sections of the PVS User
Guide, starting on page 23.

M-x prut, for example, applies the specified prover strategy to
all the proofs in the given theory that do not already have a
proof.  If you've already proved the theorems interactively,
you'll either have to remove the proofs (M-x remove-proof, see
P27) or can just copy the specification to a new theory.

2.  The pvs-strategies files are loaded from the current (context)
directory and the user's home directory.   See the prover manual,
page 105.

3.  A simple strategy that just calls a succession of other strategies
looks like this

(defstep grnd-repl-assrt ()
(then (ground) (repeat (replace*)) (assert))
"Does GROUND, then REPEAT* (repeatedly) followed by ASSERT"
"Replacing all LHS by RHS and using propositional calculus and
decision procedures"
)

You'd then call this with (grnd-repl-assrt)

The "then" rule just concatenates a number of more basic
strategies.  The first string is what's printed by (help
grnd-repl-assrt) and the second is what's printed during a proof.

A simple one that takes an argument is the following.

(defstep use-grnd-repl-assrt (lemma)
(then (use lemma :polarity? t) (ground) (repeat (replace*))
(assert))
"Uses named LEMMA, then does GROUND, then REPEAT* (repeatedly)
followed by ASSERT"
"Using lemma ~a, Replacing all LHS by RHS and using propositional
calculus and decision procedures"
)

You'd call this with (use-grnd-repl-assrt "foo") where foo is a
lemma name.

You can look at the definitions of the built-in strategies to see
how more complicated things are done.

The pvs-strategies files are loaded automatically at the beginning
of a proof if the file system indicates they've been changed.  You
can force them to be loaded in the middle of a proof by M-x