%-----------------------------------------------------------------------------
% Conversions between sequences of countable length defined as coalgebraic
% datatypes and the prelude finseq 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_finseq[T:
TYPE]:
THEORY
BEGIN
IMPORTING finite_sequences[T], csequence_nth[T]
n:
VAR nat
fs:
VAR finseq
fseq:
VAR finite_csequence
% Convert a finseq to a finite_csequence
from_finseq(fs):
RECURSIVE finite_csequence =
IF fs`length = 0
THEN empty_cseq
ELSE add(fs`seq(0),
from_finseq((# length := fs`length - 1,
seq
:=
LAMBDA (x: below[fs`length - 1]):
fs`seq(x + 1) #)))
ENDIF
MEASURE fs`length
from_finseq_length:
THEOREM FORALL fs: length(from_finseq(fs)) = fs`length
from_finseq_index:
THEOREM
FORALL fs, n: index?(from_finseq(fs))(n)
IFF n < fs`length
from_finseq_nth:
THEOREM
FORALL fs, (n: below[fs`length]): nth(from_finseq(fs), n) = fs`seq(n)
% Convert a finite_csequence to a finseq
to_finseq(fseq): finseq =
(# length := length(fseq),
seq :=
LAMBDA (x: below[length(fseq)]): nth(fseq, x) #)
to_finseq_length:
THEOREM
FORALL fseq: to_finseq(fseq)`length = length(fseq)
to_finseq_index:
THEOREM
FORALL fseq, n: n < to_finseq(fseq)`length
IFF index?(fseq)(n)
to_finseq_nth:
THEOREM
FORALL fseq, (n: indexes(fseq)): to_finseq(fseq)`seq(n) = nth(fseq, n)
% Applying both conversions gives you back what you started with
to_from_finseq:
THEOREM FORALL fs: to_finseq(from_finseq(fs)) = fs
from_to_finseq:
THEOREM FORALL fseq: from_finseq(to_finseq(fseq)) = fseq
END csequence_finseq
