%-----------------------------------------------------------------------------
% Finite and infinite sequences, and also the nonempty subtype, part of the
% theory of 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_props[T:
TYPE]:
THEORY
BEGIN
IMPORTING csequence[T]
t:
VAR T
p, q:
VAR pred[T]
cseq, cseq_rest:
VAR csequence
n, m:
VAR nat
% This predicate is TRUE iff cseq is finite and of length n
has_length(cseq, n):
RECURSIVE bool =
IF empty?(cseq)
THEN n = 0
ELSE n > 0
AND has_length(rest(cseq), n - 1)
ENDIF
MEASURE n
has_length_injective:
THEOREM
FORALL cseq, n, m:
has_length(cseq, n)
AND has_length(cseq, m)
IMPLIES n = m
% This predicate is TRUE iff cseq is finite
is_finite(cseq):
INDUCTIVE bool = empty?(cseq)
OR is_finite(rest(cseq))
is_finite_def:
THEOREM
FORALL cseq: is_finite(cseq)
IFF (
EXISTS n: has_length(cseq, n))
is_infinite(cseq):
MACRO bool =
NOT is_finite(cseq)
% Various useful subtypes of the csequence type
finite_csequence:
TYPE+ = (is_finite)
CONTAINING empty_cseq
infinite_csequence:
TYPE = (is_infinite)
empty_csequence:
TYPE+ = (empty?)
CONTAINING empty_cseq
nonempty_csequence:
TYPE = (
nonempty?)
nonempty_finite_csequence:
TYPE = {cseq: finite_csequence |
nonempty?(cseq)}
% Judgements relating the types
empty_csequence_is_finite:
JUDGEMENT
empty_csequence SUBTYPE_OF finite_csequence
infinite_csequence_is_nonempty:
JUDGEMENT
infinite_csequence SUBTYPE_OF nonempty_csequence
% Properties of some and every
pred_NOT(p)(t): bool =
NOT p(t)
pred_AND(p, q)(t): bool = p(t)
AND q(t)
pred_OR(p, q)(t): bool = p(t)
OR q(t)
pred_IMPLIES(p, q)(t): bool = p(t)
IMPLIES q(t)
some_every_rew:
THEOREM
FORALL p, cseq: some(p)(cseq)
IFF NOT every(pred_NOT(p))(cseq)
every_some_rew:
THEOREM
FORALL p, cseq: every(p)(cseq)
IFF NOT some(pred_NOT(p))(cseq)
some_implies:
THEOREM
FORALL cseq, p, q:
(
FORALL t: pred_IMPLIES(p, q)(t))
AND some(p)(cseq)
IMPLIES
some(q)(cseq)
every_implies:
THEOREM
FORALL cseq, p, q:
(
FORALL t: pred_IMPLIES(p, q)(t))
AND every(p)(cseq)
IMPLIES
every(q)(cseq)
END csequence_props
