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

*To*: pvs@csl.sri.com*Subject*: More questions about predicate subtypes*From*: Kellom{ki Pertti <pk@cs.tut.fi>*Date*: Tue, 24 Apr 2001 15:42:12 +0300 (EET DST)*Sender*: pvs-owner@csl.sri.com

I have some more questions about predicate subtypes. What I am trying to do is to use predicate subtypes to constrain more than one argument of a function. The following theory hopefully illustrates what I am doing: test: THEORY BEGIN obj: TYPE+ t: TYPE+ p: [obj, t -> bool] i: [(p) -> int] f: [(p) -> int] = LAMBDA (x: obj, st: t): i(x, st) + 1 g(x: obj, st: (LAMBDA (s: t): p(x, s))): int = i(x, st) + 1 END test I am trying to express a function of type [(p) -> int]. I would prefer the form in which f is written, but I get a TCC f_TCC1: OBLIGATION FORALL (st: t, x: obj): p(x, st); and I do not know how to get to the type information that says that p(x,st) is true. Skolemizing and doing (typepred "(x!1, st!1)") does not work. For g I get the TCC g_TCC1: OBLIGATION FORALL (x: obj, st: (LAMBDA (s: t): p(x, s))): p(x, st); which is provable. My questions now are: - Can f_TCC1 be proved? - Is restricting the last argument using dependent types as in g completely equivalent to giving the restriction as in the declaration of f? Thanks, Pertti

**Follow-Ups**:**Re: More questions about predicate subtypes***From:*Hendrik Tews <tews@tcs.inf.tu-dresden.de>

- Prev by Date:
**Help needed for learning PVS** - Next by Date:
**Re: More questions about predicate subtypes** - Prev by thread:
**Help needed for learning PVS** - Next by thread:
**Re: More questions about predicate subtypes** - Index(es):