Quelle  fseqs_ops.pvs

fseqs_ops [T: TYPE+]: THEORY
%------------------------------------------------------------------------
%
%  Defines some convenient operations over finite sequences
%
%  EXPERIMENTAL
%
%------------------------------------------------------------------------
BEGIN

  IMPORTING  fseqs[T]

  fs: VAR fseq
  nefs: VAR ne_fseq
  i,n: VAR nat
  x: VAR T

  first(fs): T = fs`seq(0)

  rest(fs): fseq = fs^(1,l(fs))

  delete(n, nefs): fseq = IF n < l(nefs) THEN
                                 (# length := l(nefs) - 1,
                                    seq := (LAMBDA i: (IF i < n THEN nefs(i) 
                                                    ELSE nefs(i + 1) ENDIF))
                                  #)
                             ELSE nefs
                             ENDIF


  insert(x, n, fs): fseq = IF n <= l(fs) THEN 
                                (# length := l(fs) + 1,
                  seq := (LAMBDA i: IF i < n THEN fs(i)
                                   ELSIF i = n THEN x
                                   ELSE fs(i - 1) ENDIF)
                                 #)
                              ELSE
                                 fs
                              ENDIF

  add(x, fs): fseq = insert(x, 0, fs)


  addend(x:T,fs:fseq): fseq = (# length := l(fs) + 1,
                                     seq := (LAMBDA (ii: nat):
                                       IF ii < l(fs) THEN seq(fs)(ii) 
                                       ELSIF ii < l(fs) + 1 THEN  x 
                                       ELSE default ENDIF)
                                    #)



  insert_delete: LEMMA n < l(nefs) IMPLIES
                          insert(nefs`seq(n), n, delete(n, nefs)) = nefs

  add_first_rest: LEMMA add(first(nefs), rest(nefs)) = nefs


  p: VAR pred[T]
  every(p)(fs): bool = (FORALL n: n < l(fs) IMPLIES p(fs(n)))

  every(p, fs): bool = (FORALL n: n < l(fs) IMPLIES p(fs(n)))

  some(p)(fs): bool = (EXISTS n: n < l(fs) IMPLIES p(fs(n)))

  some(p, fs): bool = (EXISTS n: n < l(fs) IMPLIES p(fs(n)))


  % This definition looks a little strange. The following lemma can be easily proved.

  some_p_trivial: LEMMA some(p,fs)


  F: VAR [T -> T]

  map(F,fs): fseq = (# length := length(fs),
                            seq := (LAMBDA i: IF i < length(fs) THEN
                                                 F(fs`seq(i))
                                              ELSE
                                                 default
                                              ENDIF)
                          #)

END fseqs_ops