%-----------------------------------------------------------------------------
% Properties of the add operator on sequences of countable length 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_add[T: TYPE]: THEORY
 BEGIN

  IMPORTING csequence_nth[T]

  n: VAR nat
  t: VAR T
  p: VAR pred[T]
  cseq: VAR csequence
  fseq: VAR finite_csequence
  iseq: VAR infinite_csequence

  add_finite: JUDGEMENT add(t, fseq) HAS_TYPE nonempty_finite_csequence

  add_infinite: JUDGEMENT add(t, iseq) HAS_TYPE infinite_csequence

  add_length: THEOREM
    FORALL t, fseq: length(add(t, fseq)) = length(fseq) + 1

  add_index: THEOREM
    FORALL t, cseq, n:
      index?(add(t, cseq))(n) IFF n = 0 OR index?(cseq)(n - 1)

  add_nth: THEOREM
    FORALL t, cseq, (n: indexes(cseq)):
      nth(add(t, cseq), n + 1) = nth(cseq, n)

  add_last: THEOREM
    FORALL t, fseq:
      last(add(t, fseq)) = IF empty?(fseq) THEN t ELSE last(fseq) ENDIF

  add_some: THEOREM
    FORALL t, cseq, p: some(p)(add(t, cseq)) IFF p(t) OR some(p)(cseq)    

  add_every: THEOREM
    FORALL t, cseq, p: every(p)(add(t, cseq)) IFF p(t) AND every(p)(cseq)

 END csequence_add