%-----------------------------------------------------------------------------
% Split a sequence of countable length into a sequence containing the
% even-numbered elements and a sequence containing the odd-numbered elements.
%
% 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_split[T: TYPE]: THEORY
BEGIN
IMPORTING csequence_nth[T], csequence_codt_coreduce[T, csequence]
t: VAR T
p: VAR pred[T]
n: VAR nat
cseq, cseq1, cseq2: VAR csequence
nseq: VAR nonempty_csequence
fseq: VAR finite_csequence
iseq: VAR infinite_csequence
split_left_struct(cseq): csequence_struct =
IF empty?(cseq) THEN inj_empty_cseq
ELSE inj_add(first(cseq),
IF empty?(rest(cseq)) THEN empty_cseq
ELSE rest(rest(cseq))
ENDIF)
ENDIF
split_right_struct(cseq): csequence_struct =
IF empty?(cseq) OR empty?(rest(cseq)) THEN inj_empty_cseq
ELSE inj_add(first(rest(cseq)), rest(rest(cseq)))
ENDIF
split(cseq): [csequence, csequence] =
(coreduce(split_left_struct)(cseq),
coreduce(split_right_struct)(cseq))
split_empty_left: THEOREM
FORALL cseq: empty?(split(cseq)`1) IFF empty?(cseq)
split_empty_right: THEOREM
FORALL cseq:
empty?(split(cseq)`2) IFF empty?(cseq) OR empty?(rest(cseq))
split_nonempty_left: THEOREM
FORALL cseq: nonempty?(split(cseq)`1) IFF nonempty?(cseq)
split_nonempty_right: THEOREM
FORALL cseq:
nonempty?(split(cseq)`2) IFF nonempty?(cseq) AND nonempty?(rest(cseq))
split_first_left: THEOREM FORALL nseq: first(split(nseq)`1) = first(nseq)
split_first_right: THEOREM
FORALL nseq:
nonempty?(rest(nseq)) IMPLIES first(split(nseq)`2) = first(rest(nseq))
split_rest_left: THEOREM
FORALL nseq:
rest(split(nseq)`1) =
IF empty?(rest(nseq)) THEN empty_cseq
ELSE split(rest(rest(nseq)))`1
ENDIF
split_rest_right: THEOREM
FORALL nseq:
nonempty?(rest(nseq)) IMPLIES
rest(split(nseq)`2) = split(rest(rest(nseq)))`2
split_rest_swap_left: THEOREM
FORALL nseq: split(rest(nseq))`1 = split(nseq)`2
split_rest_swap_right: THEOREM
FORALL nseq: split(rest(nseq))`2 = rest(split(nseq)`1)
split_finite: JUDGEMENT
split(fseq) HAS_TYPE [finite_csequence, finite_csequence]
split_infinite: JUDGEMENT
split(iseq) HAS_TYPE [infinite_csequence, infinite_csequence]
split_length_left: THEOREM
FORALL fseq: length(split(fseq)`1) = ceiling(length(fseq) / 2)
split_length_right: THEOREM
FORALL fseq: length(split(fseq)`2) = floor(length(fseq) / 2)
split_length: THEOREM
FORALL fseq:
length(fseq) = length(split(fseq)`1) + length(split(fseq)`2)
split_index_left: THEOREM
FORALL cseq, n: index?(split(cseq)`1)(n) IFF index?(cseq)(2 * n)
split_index_right: THEOREM
FORALL cseq, n: index?(split(cseq)`2)(n) IFF index?(cseq)(2 * n + 1)
split_nth_left: THEOREM
FORALL cseq, (n: indexes(split(cseq)`1)):
nth(split(cseq)`1, n) = nth(cseq, 2 * n)
split_nth_right: THEOREM
FORALL cseq, (n: indexes(split(cseq)`2)):
nth(split(cseq)`2, n) = nth(cseq, 2 * n + 1)
split_add: THEOREM
FORALL cseq, t:
split(add(t, cseq)) = (add(t, split(cseq)`2), split(cseq)`1)
split_last_left: THEOREM
FORALL fseq:
nonempty?(split(fseq)`1) IMPLIES
last(split(fseq)`1) =
IF odd?(length(fseq)) THEN last(fseq)
ELSE nth(fseq, length(fseq) - 2)
ENDIF
split_last_right: THEOREM
FORALL fseq:
nonempty?(split(fseq)`2) IMPLIES
last(split(fseq)`2) =
IF even?(length(fseq)) THEN last(fseq)
ELSE nth(fseq, length(fseq) - 2)
ENDIF
split_extensionality: THEOREM
FORALL cseq1, cseq2: split(cseq1) = split(cseq2) IMPLIES cseq1 = cseq2
split_some: THEOREM
FORALL cseq, p:
some(p)(cseq) IFF some(p)(split(cseq)`1) OR some(p)(split(cseq)`2)
split_every: THEOREM
FORALL cseq, p:
every(p)(cseq) IFF every(p)(split(cseq)`1) AND every(p)(split(cseq)`2)
END csequence_split
¤ Dauer der Verarbeitung: 0.20 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.
|
