%-----------------------------------------------------------------------------
% Subsequences of sequences of countable length.
%
% Author: Jerry James <[email protected]>
%
% 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_subsequence[T: TYPE]: THEORY
BEGIN
IMPORTING csequence_prefix[T], csequence_suffix[T]
p: VAR pred[T]
n, m: VAR nat
cseq, cseq1, cseq2: VAR csequence
nseq, nseq1, nseq2: VAR nonempty_csequence
fseq, fseq1, fseq2: VAR finite_csequence
subsequence?(cseq1, cseq2): COINDUCTIVE bool =
empty?(cseq1) OR
(EXISTS (n: indexes(cseq2)):
first(cseq1) = nth(cseq2, n) AND
subsequence?(rest(cseq1), suffix(cseq2, n + 1)))
subsequence?(cseq2)(cseq1): MACRO bool = subsequence?(cseq1, cseq2)
subsequence?_empty_left: THEOREM
FORALL cseq: subsequence?(empty_cseq, cseq)
subsequence?_empty_right: THEOREM
FORALL cseq: subsequence?(cseq, empty_cseq) IFF empty?(cseq)
subsequence?_rest1: THEOREM
FORALL nseq1, nseq2:
subsequence?(nseq1, nseq2) IMPLIES
subsequence?(rest(nseq1), rest(nseq2))
subsequence?_rest2: THEOREM
FORALL cseq, nseq:
subsequence?(cseq, rest(nseq)) IMPLIES subsequence?(cseq, nseq)
subsequence?_extensionality: THEOREM
FORALL nseq1, nseq2:
subsequence?(rest(nseq1), rest(nseq2)) AND
first(nseq1) = first(nseq2)
IMPLIES subsequence?(nseq1, nseq2)
subsequence?_finite: THEOREM
FORALL cseq, fseq: subsequence?(cseq, fseq) IMPLIES is_finite(cseq)
subsequence?_nth: THEOREM
FORALL cseq1, cseq2:
subsequence?(cseq1, cseq2) IMPLIES
(FORALL (n: indexes(cseq1)):
EXISTS (m: indexes(cseq2)):
nth(cseq1, n) = nth(cseq2, m) AND
subsequence?(suffix(cseq1, n + 1), suffix(cseq2, m + 1)))
subsequence?_concatenate_left: THEOREM
FORALL cseq1, cseq2:
subsequence?(cseq1, cseq2) IMPLIES
(FORALL fseq: subsequence?(cseq1, fseq o cseq2))
subsequence?_concatenate_right: THEOREM
FORALL cseq1, cseq2:
subsequence?(cseq1, cseq2) IMPLIES
(FORALL cseq: subsequence?(cseq1, cseq2 o cseq))
subsequence?_prefix: THEOREM
FORALL cseq, n, m:
n <= m IMPLIES subsequence?(prefix(cseq, n), prefix(cseq, m))
subsequence?_suffix: THEOREM
FORALL cseq, n, m:
n <= m IMPLIES subsequence?(suffix(cseq, m), suffix(cseq, n))
subsequence?_length: THEOREM
FORALL fseq1, fseq2:
subsequence?(fseq1, fseq2) IMPLIES length(fseq1) <= length(fseq2)
subsequence?_length_eq: THEOREM
FORALL fseq1, fseq2:
subsequence?(fseq1, fseq2) AND length(fseq1) = length(fseq2) IMPLIES
fseq1 = fseq2
% Note that subsequence? is not a partial order, because it is not
% antisymmetric. These two sequences are subsequences of each other,
% but are not equal:
%
% 1, 2, 1, 2, 1, 2, ...
% 2, 1, 2, 1, 2, 1, ...
subsequence?_is_preorder: JUDGEMENT
subsequence? HAS_TYPE (preorder?[csequence])
% However, subsequence? is a partial order when restricted to finite
% sequences.
subsequence?_finite_antisymmetric: THEOREM
partial_order?[finite_csequence]
(restrict
[[csequence, csequence], [finite_csequence, finite_csequence],
bool]
(subsequence?))
prefix?_is_subsequence?: JUDGEMENT
(prefix?(cseq)) SUBTYPE_OF (subsequence?(cseq))
suffix?_is_subsequence?: JUDGEMENT
(suffix?(cseq)) SUBTYPE_OF (subsequence?(cseq))
subsequence?_some: THEOREM
FORALL cseq1, cseq2, p:
subsequence?(cseq1, cseq2) AND some(p)(cseq1) IMPLIES some(p)(cseq2)
subsequence?_every: THEOREM
FORALL cseq1, cseq2, p:
subsequence?(cseq1, cseq2) AND every(p)(cseq2) IMPLIES every(p)(cseq1)
% An alternative characterization of subsequences: there exists a
% monotonically increasing function from the indexes of the "smaller"
% sequence to the indexes of the "larger" sequence such that the
% mapped elements are equal
subsequence_func(cseq2, (cseq1: (subsequence?(cseq2))))
(n: indexes(cseq1)): RECURSIVE
indexes(cseq2) =
LET index =
min[indexes(cseq2)]
({i: indexes(cseq2) | first(cseq1) = nth(cseq2, i)})
IN
IF n = 0 THEN index
ELSE index + 1 +
subsequence_func(suffix(cseq2, index + 1), rest(cseq1))(n - 1)
ENDIF
MEASURE n
subsequence_func_monotonic: LEMMA
FORALL cseq1, cseq2, (n, m: indexes(cseq1)):
subsequence?(cseq1, cseq2) AND n < m IMPLIES
subsequence_func(cseq2, cseq1)(n) < subsequence_func(cseq2, cseq1)(m)
subsequence_func_nth: LEMMA
FORALL cseq1, cseq2, (n: indexes(cseq1)):
subsequence?(cseq1, cseq2) IMPLIES
nth(cseq1, n) = nth(cseq2, subsequence_func(cseq2, cseq1)(n))
subsequence?_def: THEOREM
FORALL cseq1, cseq2:
subsequence?(cseq1, cseq2) IFF
(EXISTS (f: [indexes(cseq1) -> indexes(cseq2)]):
(FORALL (i1, i2: indexes(cseq1)): i1 < i2 IMPLIES f(i1) < f(i2))
AND
(FORALL (i: indexes(cseq1)): nth(cseq1, i) = nth(cseq2, f(i))))
END csequence_subsequence
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
