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

*To*: pvs-help@xxxxxxxxxxx*Subject*: [PVS-Help] Circular dependencies in judgements of PVS 4.0*From*: Henning Thielemann <lemming@xxxxxxxxxxxxxxxxxxxxx>*Date*: Wed, 12 Sep 2007 17:56:58 +0200 (CEST)*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>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

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

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