SSL csequence_constant.pvs

%-----------------------------------------------------------------------------
% Constant sequences, both finite and infinite, defined as coalgebraic
% datatypes.
%
% 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_constant[T: TYPE]: THEORY
 BEGIN

  IMPORTING csequence_singleton[T], csequence_codt_coreduce[T, T]

  t: VAR T
  p: VAR pred[T]
  n, m: VAR nat

  % The finite sequence consisting of n copies of a single element
  constant_cseq(t, n): RECURSIVE finite_csequence =
    IF n = 0 THEN empty_cseq ELSE add(t, constant_cseq(t, n - 1)) ENDIF
     MEASURE n

  constant_cseq_empty: THEOREM
    FORALL t, n: empty?(constant_cseq(t, n)) IFF n = 0

  constant_cseq_1: THEOREM FORALL t: constant_cseq(t, 1) = singleton_cseq(t)

  constant_cseq_first: THEOREM
    FORALL t, n: n > 0 IMPLIES first(constant_cseq(t, n)) = t

  constant_cseq_rest: THEOREM
    FORALL t, n:
      n > 0 IMPLIES rest(constant_cseq(t, n)) = constant_cseq(t, n - 1)

  constant_cseq_length: THEOREM FORALL t, n: length(constant_cseq(t, n)) = n

  constant_cseq_index: THEOREM
    FORALL t, n, m: index?(constant_cseq(t, n))(m) IFF m < n

  constant_cseq_nth: THEOREM
    FORALL t, n, (m: below[n]): nth(constant_cseq(t, n), m) = t

  constant_cseq_add: THEOREM
    FORALL t, n: add(t, constant_cseq(t, n)) = constant_cseq(t, n + 1)

  constant_cseq_last: THEOREM
    FORALL t, n: n > 0 IMPLIES last(constant_cseq(t, n)) = t

  constant_cseq_some: THEOREM
    FORALL t, n, p: some(p)(constant_cseq(t, n)) IFF n > 0 AND p(t)

  constant_cseq_every: THEOREM
    FORALL t, n, p: every(p)(constant_cseq(t, n)) IFF n = 0 OR p(t)


  % The infinite sequence consisting of a single element
  constant_cseq_struct(t): csequence_struct[T, T] = inj_add(t, t)

  constant_cseq(t): infinite_csequence = coreduce(constant_cseq_struct)(t)

  constant_cseq_inf_first: THEOREM FORALL t: first(constant_cseq(t)) = t

  constant_cseq_inf_rest: THEOREM
    FORALL t: rest(constant_cseq(t)) = constant_cseq(t)

  constant_cseq_inf_nth: THEOREM FORALL t, n: nth(constant_cseq(t), n) = t

  constant_cseq_inf_add: THEOREM
    FORALL t, n: add(t, constant_cseq(t)) = constant_cseq(t)

  constant_cseq_inf_some: THEOREM
    FORALL t, p: some(p)(constant_cseq(t)) IFF p(t)

  constant_cseq_inf_every: THEOREM
    FORALL t, p: every(p)(constant_cseq(t)) IFF p(t)

 END csequence_constant