%-----------------------------------------------------------------------------
% Singleton sequences, 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_singleton[T: TYPE]: THEORY
 BEGIN

  IMPORTING csequence_nth[T]

  t: VAR T
  p: VAR pred[T]
  n: VAR nat
  cseq: VAR csequence

  singleton_cseq?(cseq): bool = nonempty?(cseq) AND empty?(rest(cseq))

  singleton_is_nonempty_finite: JUDGEMENT
    (singleton_cseq?) SUBTYPE_OF nonempty_finite_csequence

  singleton_cseq_length: THEOREM
    FORALL cseq: singleton_cseq?(cseq) IMPLIES length(cseq) = 1

  singleton_cseq_index: THEOREM
    FORALL (single: (singleton_cseq?)), n: index?(single)(n) IFF n = 0

  singleton_cseq(t): (singleton_cseq?) = add(t, empty_cseq)

  singleton_def: THEOREM
    FORALL cseq:
      singleton_cseq?(cseq) IMPLIES cseq = singleton_cseq(first(cseq))

  singleton_cseq_first: THEOREM FORALL t: first(singleton_cseq(t)) = t

  singleton_cseq_rest: THEOREM FORALL t: rest(singleton_cseq(t)) = empty_cseq

  singleton_cseq_last: THEOREM FORALL t: last(singleton_cseq(t)) = t

  singleton_cseq_some: THEOREM
    FORALL t, p: some(p)(singleton_cseq(t)) IFF p(t)

  singleton_cseq_every: THEOREM
    FORALL t, p: every(p)(singleton_cseq(t)) IFF p(t)

 END csequence_singleton