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

Re: subset relationship in types



> 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