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

What's the context for TCC proofs?

I have a question about discharging TCC's.

1.  I created an equivalence relation theory, EQUIV, with the intent of
having it imported by different theories, so that different relations
could be used to instantiate the basic properties of equivalence
relations. So all I put in EQUIV itself were assumptions that the
instantiating relation would have to be refl., symm. & trans. 

2. I then created a theory of a particular relation on strings, MATCH,
that I would use to instantiate the properties assumed for equivalence
relations in the first theory.  In this second theory, all I do is declare
MATCH, declare the types of its instances, and provide an axiom
stating necessary and sufficient conditions on MATCH.

3. Lastly, I created a test theory whose only function was to import
EQUIV, and MATCH theory (MATCH theory first) with MATCH serving as actual
passed in for the parameters of EQUIV.

Just as desired, when I typechecked the test theory, 3 TCCs were
generated, one for showing MATCH is reflexive, one for showing MATCH is
symmetric, one for showing MATCH is transitive.  PVS is cool.  But then,
when I set out to prove the first TCC, I tried to appeal to an instance of
the axiom governing MATCH and I got error messages.  First, when my
reference to the name of the axiom was unqualified, PVS said:

	Couldn't find a definition or lemma named Match
	No change on: (LEMMA "Match" ("a" "t1!1" "q" "t1!1"))

So I tried prefixing the reference to the axiom with the name of the file
containing the axiom.  Then what I got was a response saying:

	Theory Match is not in the IMPORTINGs
	Restoring the state.

I'm not sure why the lemma rule is failing here.  I would have thought
that the context for TCCs generated in typechecking a theory is just the
context for the theory itself, including any theories it imports.  Isn't
that true?

Can anyone help?  Thanks in advance,

Mark Aronszajn