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

[PVS-Help] How to define a step for splitting without generatingredundant TCCs



Dear all,

I am trying to define a PVS strategy for splitting a sequent of the
form:

X |- A and B

into the two subgoals:

X    |- A
X, A |- B

This is straightforwardly accomplished by (case "not A") and
simplifying the resulting sequents. However, doing so introduces
redundant TCCs for A, which I would like to avoid. Is there some way
of using more primitive proof functions, maybe from PVS lisp, to
achieve the same but bypassing the TCC generation?

Regards,
Johannes Eriksson

-- 
Johannes W. E. Eriksson, M.Sc.
Ph.D. Student / Turku Centre For Computer Science (TUCS)
Åbo Akademi University / Department of Information Technologies
e-mail: joheriks@abo.fi  www: http://www.abo.fi/~joheriks