Quelle  fsq.pvs

fsq[T: TYPE]: THEORY
%------------------------------------------------------------------------
%
% This theory is scaffolding for the "fseqs" finite sequences theory
%
%------------------------------------------------------------------------
BEGIN

  x,y : VAR T

  fsq: TYPE = [# length: nat, seq: [nat -> T] #]

  cnvfsq(fs: fsq): MACRO [nat -> T] = fs`seq;
  CONVERSION cnvfsq;
  CONVERSION- finseq_appl;                   %% turn off prelude finseq conversion

  l(f: fsq): MACRO nat = f`length
  seqn(f: fsq): MACRO [nat -> T]= f`seq


  %% not empty fseqs
  ne_fsq: TYPE = {s: fsq  | length(s) > 0}

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


  fsq1(t:T): fsq = (# length := 1,
                      seq := (LAMBDA (n: nat): t) #)

  const_fsq(n: nat,c:T): fsq = (# length := n,
                                  seq := (LAMBDA (n: nat): c) #)


END fsq