%-----------------------------------------------------------------------------
% Functions that generate infinite sequences.
%
% Author: Jerry James <loganjerry@gmail.com>
%
% This file and its accompanying proof file are distributed under the CC0 1.0
% Universal license: http://creativecommons.org/publicdomain/zero/1.0/.
%
% Version history:
%   2007 Feb 14: PVS 4.0 version
%   2011 May  6: PVS 5.0 version
%   2013 Jan 14: PVS 6.0 version
%-----------------------------------------------------------------------------
csequence_generate[T: TYPE]: THEORY
 BEGIN

  IMPORTING function_iterate[T], csequence_nth[T]
  IMPORTING csequence_codt_coreduce[T, [[T -> T], T]]

  n: VAR nat
  t, u: VAR T
  p: VAR pred[T]
  f, g: VAR [T -> T]
  state: VAR [[T -> T], T]

  % The generator is given a starting T, and a function that generates the
  % next T from the previous one.
  generate_struct(state): csequence_struct =
      inj_add(state`2, (state`1, state`1(state`2)))

  generate(f, t): infinite_csequence = coreduce(generate_struct)((f, t))

  generate_first: THEOREM FORALL f, t: first(generate(f, t)) = t

  generate_rest: THEOREM
    FORALL f, t: rest(generate(f, t)) = generate(f, f(t))

  generate_nth: THEOREM
    FORALL f, t, n: nth(generate(f, t), n) = iterate(f, n)(t)

  generate_add: THEOREM
    FORALL f, t, u: t = f(u) IMPLIES add(u, generate(f, t)) = generate(f, u)

  generate_some: THEOREM
    FORALL f, t, p:
      some(p)(generate(f, t)) IFF (EXISTS n: p(iterate(f, n)(t)))

  generate_every: THEOREM
    FORALL f, t, p:
      every(p)(generate(f, t)) IFF (FORALL n: p(iterate(f, n)(t)))

 END csequence_generate