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

*Subject*: Re: [PVS-Help] How to define a step for splitting without generatingredundant TCCs*From*: Jerome White <jerome@xxxxxxxxxxxxxx>*Date*: Wed, 25 Nov 2009 20:40:12 -0800*CC*: pvs-help@xxxxxxxxxxx*In-Reply-To*: <20091125235054.GB31401@jweeriks.sby.abo.fi>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <20091119135948.GA3955@jweeriks.sby.abo.fi><20091125235054.GB31401@jweeriks.sby.abo.fi>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-Agent*: Thunderbird 2.0.0.23 (X11/20090817)

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

**Follow-Ups**:**Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs***From:*Johannes Eriksson

**References**:**[PVS-Help] How to define a step for splitting without generatingredundant TCCs***From:*Johannes Eriksson

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

- Prev by Date:
**Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs** - Next by Date:
**Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs** - Prev by thread:
**Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs** - Next by thread:
**Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs** - Index(es):