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

*To*: Borzoo Bonakdarpour <borzoo@cse.msu.edu>*Subject*: Re: subset relationship in types*From*: John Rushby <rushby@csl.sri.com>*Date*: Fri, 14 Mar 2003 17:02:28 PST*Cc*: John Rushby <rushby@csl.sri.com>, <pvs-help@csl.sri.com>*In-Reply-To*: Your message of Fri, 14 Mar 2003 19:44:03 -0500 (EST)*Sender*: pvs-help-owner@csl.sri.com

> No, I mean "subset". For example: > > set1 : TYPE = finite_set[T] > set2 : TYPE = finite-set[T] > > I need to write an ASSUMPTION, such that any variable from type of set2 > would be subset of any variable from type of set1. > Then how about the following: foo[T: TYPE]:THEORY BEGIN set1: TYPE = finite_set[T] set2: TYPE = {t: finite_set[T]| FORALL (s:set1): subset?(t,s)} a: VAR set1 b: VAR set2 test: LEMMA subset?(b,a) END foo You can then prove test from the type predicate on b. John

- Prev by Date:
**Re: subset relationship in types** - Next by Date:
**a question** - Prev by thread:
**Re: subset relationship in types** - Next by thread:
**Re: rewrite rule for expressions inside LAMBDA** - Index(es):