%-----------------------------------------------------------------------------
% Conversions between sequences of countable length and the prelude list 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_list[T:
TYPE]:
THEORY
BEGIN
IMPORTING list[T], list_props[T], csequence_nth[T]
n:
VAR nat
l:
VAR list
fseq:
VAR finite_csequence
% Convert a list to a finite_csequence
from_list(l):
RECURSIVE finite_csequence =
IF null?(l)
THEN empty_cseq
ELSE add(car(l), from_list(cdr(l)))
ENDIF
MEASURE l
BY <<
from_list_length:
THEOREM FORALL l: length(from_list(l)) = length(l)
from_list_index:
THEOREM
FORALL l, n: index?(from_list(l))(n)
IFF n < length(l)
from_list_nth:
THEOREM
FORALL l, (n: below[length(l)]): nth(from_list(l), n) = nth(l, n)
% Convert a finite_csequence to a list
to_list(fseq):
RECURSIVE list =
IF empty?(fseq)
THEN null
ELSE cons(first(fseq), to_list(rest(fseq)))
ENDIF
MEASURE length(fseq)
to_list_length:
THEOREM FORALL fseq: length(to_list(fseq)) = length(fseq)
to_list_index:
THEOREM
FORALL fseq, n: n < length(to_list(fseq))
IFF index?(fseq)(n)
to_list_nth:
THEOREM
FORALL fseq, (n: indexes(fseq)): nth(to_list(fseq), n) = nth(fseq, n)
% Applying both conversions gives you back what you started with
to_from_list:
THEOREM FORALL l: to_list(from_list(l)) = l
from_to_list:
THEOREM FORALL fseq: from_list(to_list(fseq)) = fseq
END csequence_list
