%-----------------------------------------------------------------------------
% Flatten, an operator that takes a sequence of sequences, and concatenates
% the elements to form a single sequence 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_flatten[T: TYPE]: THEORY
BEGIN
IMPORTING csequence_prefix_suffix[T], csequence_filter[csequence[T]]
nonempty_seq_seq: TYPE = {x: csequence[csequence[T]] | every(nonempty?)(x)}
p: VAR pred[T]
n: VAR nat
tseq: VAR csequence[T]
cseq: VAR csequence[csequence[T]]
eseq: VAR empty_csequence[csequence[T]]
nseq: VAR nonempty_seq_seq
% A result we need several times in the ensuing proofs
some_every_empty: LEMMA
FORALL cseq: every(empty?)(cseq) IFF NOT some(nonempty?)(cseq)
flatten_struct(nseq): csequence_struct[T, nonempty_seq_seq] =
IF empty?(nseq) THEN inj_empty_cseq[T, nonempty_seq_seq]
ELSE inj_add[T, nonempty_seq_seq]
(first(first(nseq)),
IF empty?(rest(first(nseq))) THEN rest(nseq)
ELSE add(rest(first(nseq)), rest(nseq))
ENDIF)
ENDIF
flatten(cseq): csequence[T] =
coreduce(flatten_struct)(filter(cseq, nonempty?))
flatten_empty: THEOREM
FORALL cseq: empty?(flatten(cseq)) IFF every(empty?)(cseq)
flatten_empty_cseq: COROLLARY FORALL eseq: empty?(flatten(eseq))
flatten_nonempty: THEOREM
FORALL cseq: nonempty?(flatten(cseq)) IFF some(nonempty?)(cseq)
flatten_filter: THEOREM
FORALL cseq: flatten(filter(cseq, nonempty?)) = flatten(cseq)
flatten_reduce: THEOREM
FORALL cseq:
empty?(cseq) OR
nonempty?(first(cseq)) OR flatten(cseq) = flatten(rest(cseq))
flatten_rest: THEOREM
FORALL cseq:
nonempty?(flatten(cseq)) IMPLIES
rest(flatten(cseq)) =
flatten(add(rest(first(filter(cseq, nonempty?))),
rest(filter(cseq, nonempty?))))
flatten_rest2: THEOREM
FORALL cseq:
empty?(cseq) OR
empty?(first(cseq)) OR
rest(flatten(cseq)) = flatten(add(rest(first(cseq)), rest(cseq)))
flatten_first: THEOREM
FORALL cseq:
nonempty?(flatten(cseq)) IMPLIES
first(flatten(cseq)) = first(first(filter(cseq, nonempty?)))
flatten_suffix: THEOREM
FORALL cseq:
some(nonempty?)(cseq) IMPLIES
flatten(cseq) = flatten(suffix(cseq, first_p(nonempty?, cseq)))
% I would really like to define flatten like this:
% flatten(cseq) = reduce(o)(cseq)
% but this theorem is as close as I can come
flatten_concatenate: THEOREM
FORALL cseq:
nonempty?(cseq) IMPLIES
flatten(cseq) = first(cseq) o flatten(rest(cseq))
flatten_rest_suffix: THEOREM
FORALL cseq:
nonempty?(flatten(cseq)) IMPLIES
LET first = first_p(nonempty?, cseq) IN
rest(flatten(cseq)) =
flatten(add(rest(nth(cseq, first)), suffix(cseq, first + 1)))
flatten_finite: THEOREM
FORALL cseq:
is_finite(flatten(cseq)) IFF
is_finite(filter(cseq, nonempty?)) AND every(is_finite)(cseq)
flatten_infinite: THEOREM
FORALL cseq:
is_infinite(flatten(cseq)) IFF
is_infinite(filter(cseq, nonempty?)) OR some(is_infinite)(cseq)
finite_flatten_csequence: TYPE = {cseq | is_finite(flatten(cseq))}
fseq: VAR finite_flatten_csequence
length_of_flatten(fseq): RECURSIVE nat =
IF empty?(flatten(fseq)) THEN 0
ELSE length(nth(fseq, first_p(nonempty?, fseq))) +
length_of_flatten(suffix(fseq, first_p(nonempty?, fseq) + 1))
ENDIF
MEASURE length(filter(fseq, nonempty?))
length_of_flatten_add: THEOREM
FORALL fseq, tseq:
is_finite(tseq) IMPLIES
length_of_flatten(add(tseq, fseq)) =
length(tseq) + length_of_flatten(fseq)
flatten_length: THEOREM
FORALL cseq:
is_finite(flatten(cseq)) IMPLIES
length(flatten(cseq)) = length_of_flatten(cseq)
flatten_some: THEOREM
FORALL cseq, p: some(p)(flatten(cseq)) IMPLIES some(some(p))(cseq)
flatten_some_finite: THEOREM
FORALL cseq, p:
every(is_finite)(cseq) IMPLIES
(some(p)(flatten(cseq)) IFF some(some(p))(cseq))
flatten_every: THEOREM
FORALL cseq, p: every(every(p))(cseq) IMPLIES every(p)(flatten(cseq))
flatten_every_finite: THEOREM
FORALL cseq, p:
every(is_finite)(cseq) IMPLIES
(every(p)(flatten(cseq)) IFF every(every(p))(cseq))
% I believe the following two theorems are true. Proving them, however,
% is a different matter. If you have a proof strategy to suggest, or a
% nicer way of stating these theorems, please contact me.
%
% flatten_some_converse: THEOREM
% FORALL cseq, p:
% (EXISTS (i: indexes(cseq)):
% some(p)(nth(cseq, i)) AND
% (FORALL (j: indexes(cseq)):
% j < i IMPLIES is_finite(nth(cseq, j))))
% IMPLIES some(p)(flatten(cseq))
%
% flatten_every_converse: THEOREM
% FORALL cseq, p:
% every(p)(flatten(cseq)) IMPLIES
% (FORALL (i: indexes(cseq)):
% (FORALL (j: indexes(cseq)):
% j < i IMPLIES is_finite(nth(cseq, j)))
% IMPLIES every(p)(nth(cseq, i)))
END csequence_flatten
¤ Dauer der Verarbeitung: 0.15 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.
|
