Quelle  subseq.pvs

%------------------------------------------------------------------------------
% Sub-sequence Properties
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Version 1.0            06/09/07  Initial Version
%------------------------------------------------------------------------------

subseq[T:TYPE]: THEORY

BEGIN

  IMPORTING sequences[T],
            reals@real_fun_preds[nat],
            orders[sequence]

  u,v,w: VAR sequence
  i:     VAR nat
  f:     VAR ({f:[nat->nat] | strict_increasing?(f)})

  subseq?(v,u): bool = EXISTS f: FORALL i: v(i) = u(f(i))

  subseq_index: LEMMA f(i) >= i

  reflexive_subseq :  LEMMA subseq?(u, u)
  transitive_subseq : LEMMA subseq?(u, v) AND subseq?(v, w) => subseq?(u, w)

END subseq