%-----------------------------------------------------------------------------
% Conversions between sequences of countable length and the prelude sequence
% type.
%
% 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_sequence[T:
TYPE]:
THEORY
BEGIN
IMPORTING sequences[T], csequence_nth[T]
IMPORTING csequence_codt_coreduce[T, sequence]
n:
VAR nat
seq:
VAR sequence
iseq:
VAR infinite_csequence
% Convert a sequence to an infinite_csequence
from_sequence_struct(seq): csequence_struct =
inj_add(seq(0),
LAMBDA n: seq(1 + n))
from_sequence(seq): infinite_csequence =
coreduce(from_sequence_struct)(seq)
from_sequence_nth:
THEOREM
FORALL seq, n: nth(from_sequence(seq), n) = seq(n)
% Convert an infinite_csequence to a sequence
to_sequence(iseq): sequence =
LAMBDA n: nth(iseq, n)
to_sequence_nth:
THEOREM
FORALL iseq, n: to_sequence(iseq)(n) = nth(iseq, n)
% Applying both conversions gives you back what you started with
to_from_sequence:
THEOREM
FORALL seq: to_sequence(from_sequence(seq)) = seq
from_to_sequence:
THEOREM
FORALL iseq: from_sequence(to_sequence(iseq)) = iseq
END csequence_sequence
