[PVS-Help] Circular dependencies in judgements of PVS 4.0

[Henning Thielemann <lemming@xxxxxxxxxxxxxxxxxxxxx>]

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