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

*To*: pvs_help list_serve <pvs-help@csl.sri.com>*Subject*: What's the context for TCC proofs?*From*: Mark Aronszajn <aronsz@csee.wvu.edu>*Date*: Fri, 17 Jul 1998 13:22:33 -0400 (EDT)

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

- Prev by Date:
**Change in emacs version** - Next by Date:
**Re: What's the context for TCC proofs?** - Prev by thread:
**Phonebook example from WIFT'95 paper not working?** - Next by thread:
**Re: What's the context for TCC proofs?** - Index(es):