%-----------------------------------------------------------------------------
% 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
