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

Re: [PVS-Help] function domains

> Is it possible to extract the domain of a function?  Eg, given 
> f: [T1 -> T2] = ...
> the expression f`domain returns the set T1.  Similarly for
> f: [{t: T1 | p(t)} -> T2] = ...
> the expression f`domain returns the set {t: T1 | p(t)}.  

domain(f) from the prelude theory for functions does this (unless T2
is typed dependently on T1).  Actually, domain(f) returns the TYPE of
the domain, not a set, so you can write constructions such as the

  T1, T2: TYPE
  p: pred[T1]
  f: [{t: T1 | p(t)} -> T2]
  foo: LEMMA FORALL (x:domain(f)): p(x)

If you want to construct a set characterizing the domain, you could
do the following, for example.

  goo: LEMMA {x:domain(f)|TRUE} = {t: T1 | p(t)}

Both these lemmas have trivial proofs.