%-----------------------------------------------------------------------------
% Constant sequences, both finite and infinite, 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_constant[T:
TYPE]:
THEORY
BEGIN
IMPORTING csequence_singleton[T], csequence_codt_coreduce[T, T]
t:
VAR T
p:
VAR pred[T]
n, m:
VAR nat
% The finite sequence consisting of n copies of a single element
constant_cseq(t, n):
RECURSIVE finite_csequence =
IF n = 0
THEN empty_cseq
ELSE add(t, constant_cseq(t, n - 1))
ENDIF
MEASURE n
constant_cseq_empty:
THEOREM
FORALL t, n: empty?(constant_cseq(t, n))
IFF n = 0
constant_cseq_1:
THEOREM FORALL t: constant_cseq(t, 1) = singleton_cseq(t)
constant_cseq_first:
THEOREM
FORALL t, n: n > 0
IMPLIES first(constant_cseq(t, n)) = t
constant_cseq_rest:
THEOREM
FORALL t, n:
n > 0
IMPLIES rest(constant_cseq(t, n)) = constant_cseq(t, n - 1)
constant_cseq_length:
THEOREM FORALL t, n: length(constant_cseq(t, n)) = n
constant_cseq_index:
THEOREM
FORALL t, n, m: index?(constant_cseq(t, n))(m)
IFF m < n
constant_cseq_nth:
THEOREM
FORALL t, n, (m: below[n]): nth(constant_cseq(t, n), m) = t
constant_cseq_add:
THEOREM
FORALL t, n: add(t, constant_cseq(t, n)) = constant_cseq(t, n + 1)
constant_cseq_last:
THEOREM
FORALL t, n: n > 0
IMPLIES last(constant_cseq(t, n)) = t
constant_cseq_some:
THEOREM
FORALL t, n, p: some(p)(constant_cseq(t, n))
IFF n > 0
AND p(t)
constant_cseq_every:
THEOREM
FORALL t, n, p: every(p)(constant_cseq(t, n))
IFF n = 0
OR p(t)
% The infinite sequence consisting of a single element
constant_cseq_struct(t): csequence_struct[T, T] = inj_add(t, t)
constant_cseq(t): infinite_csequence = coreduce(constant_cseq_struct)(t)
constant_cseq_inf_first:
THEOREM FORALL t: first(constant_cseq(t)) = t
constant_cseq_inf_rest:
THEOREM
FORALL t: rest(constant_cseq(t)) = constant_cseq(t)
constant_cseq_inf_nth:
THEOREM FORALL t, n: nth(constant_cseq(t), n) = t
constant_cseq_inf_add:
THEOREM
FORALL t, n: add(t, constant_cseq(t)) = constant_cseq(t)
constant_cseq_inf_some:
THEOREM
FORALL t, p: some(p)(constant_cseq(t))
IFF p(t)
constant_cseq_inf_every:
THEOREM
FORALL t, p: every(p)(constant_cseq(t))
IFF p(t)
END csequence_constant
