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

*To*: Henning Thielemann <lemming@xxxxxxxxxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] Circular dependencies in judgements of PVS 4.0*From*: Jeff Maddalon <j.m.maddalon@xxxxxxxx>*Date*: Wed, 12 Sep 2007 14:54:11 -0400*Cc*: pvs-help@xxxxxxxxxxx*In-Reply-To*: <Pine.SOC.4.64.0709121731230.4867@turing.informatik.uni-halle.de>*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*: <Pine.SOC.4.64.0709121731230.4867@turing.informatik.uni-halle.de>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-Agent*: Thunderbird 2.0.0.6 (X11/20070728)

I understand that you working on this to learn PVS, but the NASA PVS libraries have a large collection of multi-set results (they are called "bags"). Jeff Henning Thielemann wrote: > > Before digging into my particular problem, I have a general question. > pvs-system-guide.pdf, section "2.2 Parsing and Typechecking" states that > TCCs must be proved before theorems in a theory. If so, why am I allowed > to use lemmas of a theory in proofs of a TCC? In contrast to that, if I > prove a lemma and try to use a lemma which is defined later in the same > PVS file, the interactive PVS prover considers the later lemma as > non-existent. As a side note: I would also like to use lemmas of a theory > in proofs of TCCs of the same theory. If the order is like those of "Proof > Status", that is > lemmaA_TCC1 > lemmaA > lemmaB_TCC1 > lemmaB_TCC2 > lemmaB > would there be any chance of a circular reasoning? > > Now the particular problem: I'm working on a theory of multi-sets, which I > have designed analogously to Prelude's "sets" and "finite_sets" theories. > (I'm afraid, I'm duplicating work, however it is a nice exercise to get > started with PVS.) I have the functions 'remove', which removes one > element from a multiset, and 'remove_all', which removes all instances of > an element from a multiset. Now I have the judgements > > x: VAR T > > A: VAR finite_multiset > > finite_remove: JUDGEMENT remove(x, A) HAS_TYPE finite_multiset > > finite_remove_all: JUDGEMENT remove_all(x, A) HAS_TYPE finite_multiset > > The proofs of the statements are practically identical, because both > 'remove' and 'remove_all' generate subsets of A. However the proof of > 'finite_remove' is considered complete, whereas the one of > 'finite_remove_all' is considered incomplete, due to an circularity with > the definition of 'finite_multiset'. I compared the proof and definition > chains of 'finite_remove' and 'finite_remove_all' and I found no > differences with respect to the objects of the same module. I reduced the > proof of 'finite_remove_all' in order to see, which lemma invokation > causes the circularity. I ended up with a simple (POSTPONE) and the proof > is still considered circular (although now UNPROVED). How can I find out > more about the circularity? > > > Many thanks for the help in advance > Henning > > Martin-Luther-Universität Halle-Wittenberg, Institut für Informatik > > Tel. +49 - 345 - 55 24773 > Fax +49 - 345 - 55 27033 >

**References**:**[PVS-Help] Circular dependencies in judgements of PVS 4.0***From:*Henning Thielemann

- Prev by Date:
**Re: [PVS-Help] Circular dependencies in judgements of PVS 4.0** - Next by Date:
**[PVS-Help] problem with the RANDOM function** - Prev by thread:
**Re: [PVS-Help] Circular dependencies in judgements of PVS 4.0** - Next by thread:
**[PVS-Help] strange mapping when loading library files twice** - Index(es):