Re: PVS Problem

[John Rushby <rushby@csl.sri.com>]

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
    load-pvs-strategies (see User Guide P27).

Hope this helps you make progress.  Please ask again if you need more info.

Regards,
John Rushby