[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Question on strategies



I have what will hopefully be a simple question on defining strategies.
I've browsed the archive and chased down some links, but they were not
helpful.

Given chapter 5 of the PVS Prover Guide, it is straightforward to select
all sequent formulae that match some high level connective such as
(equality? expr).  My question is how do I get more specific.  For
example, how do I select all equality formulae that use a particular
name, such as "c!1", somewhere in the expression representing one of
their arguments.

For example, I'd like to be able to select formulae like:
    c!1 = (a,b)
or
   z = c!1`1

Any pointers or advice greatly appreciated,
Kurt