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

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



Perhaps I'm misunderstanding your question, but why not just have and l0 
that proves what you want about a(x), and use that lemma to prove l1?

jerome

Johannes Eriksson wrote:
> 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
>>
>>
>