Enum types as theory parameters?

[Pertti Kellomäki <pk@cs.tut.fi>]

Is there a way to accomplish something like the following in PVS?

th1  [ t : TYPE = {r,s} ]
		: THEORY

  BEGIN
  END th1

th2 : THEORY
BEGIN
  tt : TYPE = {p,q}
  importing th1[tt]
END th2

I.e. I would like to declare that t is an enum type with two values, and I would
like to associate p with r and q with s when instantiating th1. The closest I 
have been able to get is to make t, r, and s all be formal parameters of th1, 
but then I lose the mutual exclusion property of r and s, and I have to make
it an explicit assumption of th1.
-- 
Pertti Kellom\"aki, Tampere Univ. of Technology, Software Systems Lab