Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs

[Johannes Eriksson <joheriks@xxxxxx>]

Hi again,

I will try to make my problem a little more concrete. Say I have a
formula like:

l1: theorem a(x) and c

Additionally, assume that the application a(x) produces a complex TCC
which require some interactive theorem proving to discharge. Given
that, I would like to define a strategy split the root sequent:

|- a(x) and c

into just the two branches:

     |- a(x) 
a(x) |- c

i.e., without having to reprove the TCC from a(x), which I have to if
I use "case". How hints on how I can do it?  I know that the TCC can
be invoked as a lemma, e.g.  (use l1_TCC1), but I want to avoid that
since the strategy should work independently of the formula name.

Regards,
Johannes


* Johannes Eriksson [Thu, Nov 19, 2009 at 03:59:48PM +0200]:
> 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
> 
> 

-- 
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