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

[PVS-Help] keeping subgoal proofs ordered




Hi, I've been working in a situation where I am proving a sequent of
the form

  [-n] A or B or C or ....
  [..]
  -----------
  [..]

where "A or B or C or .." is some long disjunct (in my case coming
from an datatype declaration).  I proceed by splitting [-n], and
working on the proof for each subgoal (with antecedents A, B, C etc)
separately.  Some of these subproofs are nontrivial.  Later I decide
for whatever reason that I do not need the "C" option, and remove it
from the disjunct (or add some more disjuncts, or swap their order,
etc).  Now if I rerun the proof from the original version, the
(sub)proofs will not match the appropriate subgoals.

Is there a work around for this problem?  I could write each subgoal
that results from the split as its own theorem and use them to prove
the original, but would rather not for reasons of scalability and
theory file clutter.  A solution that appeals to me would be to
label each subgoal resulting from the split, and for pvs to
correspondingly label each (sub)proof in the proof script.  Then on
any proof rerun, subproofs are matched to correspondingly labelled
subgoals.  Is this feasible?

Rob