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

list of subtypes




Hi!
 
consider a type T and S a subtype of T.
let slist be of type list[S].
 
Is there any way to make PVS automatically
recognize that:
 
 length[T](slist) = length[S](slist),
 nth[T](slist) = nth[T](slist) .... ?
 
If it was supposed to do so, here's an example where
it fails:
 
try: THEORY
BEGIN
 
T: TYPE
p: pred[T]
S: TYPE = {s: T | p(s)}
 
SLIST: TYPE = list[S]
 
 
replace(t_list:list[T], n:below[length(t_list)], t:T) : list[T]
        = cons(t, cdr(t_list))
 
try_lemma: LEMMA
 forall (s_list:SLIST, n:below[length(s_list)], s:S) :
   length(s_list) = length(replace(s_list,n,s))
 
end try
 
.. it generates the TCC :
 
try_lemma_TCC1: OBLIGATION
  FORALL (s: S, s_list: SLIST, n: below[length(s_list)]):
    n < length[T](s_list);
 
 
 
Thank you very much!
ela



_____________________________________

Ela Teica
DDEL Lab,
Univ of Cincinnati.


Don`t be superstitious; it brings bad luck!:)

____________________________________