%-----------------------------------------------------------------------------
% Proper prefixes of sequences of countable length.
%
% 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_strict_prefix[T:
TYPE]:
THEORY
BEGIN
IMPORTING csequence_prefix[T]
p:
VAR pred[T]
n:
VAR nat
cseq, cseq1, cseq2:
VAR csequence
nseq:
VAR nonempty_csequence
fseq:
VAR finite_csequence
strict_prefix?(cseq1, cseq2):
INDUCTIVE bool =
nonempty?(cseq2)
AND
(empty?(cseq1)
OR
(first(cseq1) = first(cseq2)
AND
strict_prefix?(rest(cseq1), rest(cseq2))))
strict_prefix?(cseq2)(cseq1):
MACRO bool = strict_prefix?(cseq1, cseq2)
strict_prefix?_prefix?:
THEOREM
FORALL cseq1, cseq2:
strict_prefix?(cseq1, cseq2)
IFF
prefix?(cseq1, cseq2)
AND cseq1 /= cseq2
strict_prefix?_finite:
THEOREM
FORALL cseq1, cseq2:
strict_prefix?(cseq1, cseq2)
IMPLIES is_finite(cseq1)
strict_prefix?_first:
THEOREM
FORALL nseq, cseq:
strict_prefix?(nseq, cseq)
IMPLIES first(nseq) = first(cseq)
strict_prefix?_rest:
THEOREM
FORALL nseq, cseq:
strict_prefix?(nseq, cseq)
IMPLIES
strict_prefix?(rest(nseq), rest(cseq))
strict_prefix?_length:
THEOREM
FORALL cseq, fseq:
strict_prefix?(cseq, fseq)
IMPLIES length(cseq) < length(fseq)
strict_prefix?_index:
THEOREM
FORALL cseq1, cseq2, n:
strict_prefix?(cseq1, cseq2)
AND index?(cseq1)(n)
IMPLIES
index?(cseq2)(n)
strict_prefix?_nth:
THEOREM
FORALL cseq1, cseq2, (n: indexes(cseq1)):
strict_prefix?(cseq1, cseq2)
IMPLIES nth(cseq1, n) = nth(cseq2, n)
strict_prefix?_concatenate:
THEOREM
FORALL fseq, nseq: strict_prefix?(fseq, fseq o nseq)
strict_prefix?_def:
THEOREM
FORALL cseq1, cseq2:
strict_prefix?(cseq1, cseq2)
IFF
is_finite(cseq1)
AND (
EXISTS nseq: cseq1 o nseq = cseq2)
strict_prefix?_is_strict_order:
JUDGEMENT
strict_prefix? HAS_TYPE (strict_order?[csequence])
% Strict prefixes of a given sequence are well-ordered
strict_prefix?_well_ordered:
THEOREM
FORALL cseq:
well_ordered?(restrict
[[csequence, csequence],
[(strict_prefix?(cseq)), (strict_prefix?(cseq))],
bool]
(strict_prefix?))
strict_prefix?_prefix:
THEOREM
FORALL cseq1, cseq2:
strict_prefix?(cseq1, cseq2)
IFF
(
EXISTS n:
cseq1 = prefix(cseq2, n)
AND
(is_finite(cseq2)
IMPLIES n < length(cseq2)))
END csequence_strict_prefix
