Impressum seqs.pvs

seqs[T: TYPE]: THEORY
BEGIN

  l(f: finite_sequence[T]): MACRO nat = f`length

  ne_seqs: TYPE = {s: finite_sequence[T]  | length(s) > 0}


  in?(x: T, s: finite_sequence[T]): bool = 
              (EXISTS (ii: below(length(s))): x = seq(s)(ii))

  const_seq(n: nat,c:T): finite_sequence[T] = (# length := n,
                                                 seq := (LAMBDA (i: below(n)): c) #)

  seq1(t:T): ne_seqs = (# length := 1,
                          seq := (LAMBDA (n: below(1)): t)
                        #)


  seq2(a,b:T): ne_seqs = (# length := 2,
                          seq := (LAMBDA (n: below(2)): IF n < 1 THEN a 
                                                        ELSE b ENDIF)
                         #)

  t: VAR T
  seq1_def: LEMMA seq1(t)`seq(0) = t

  AUTO_REWRITE+ seq1_def

  fs: VAR finite_sequence[T]
  rev(fs): finite_sequence[T] = (# length := l(fs),
                           seq := (LAMBDA (i: below(l(fs))): seq(fs)(l(fs)-1-i))
                        #)


  add1(fs,t): finite_sequence[T] = (# length := l(fs) + 1,
                               seq := (LAMBDA (ii: below(l(fs)+1)):
                                    IF ii < l(fs) THEN seq(fs)(ii) 
                                    ELSE t 
                                    ENDIF)
                             #)


END seqs