%-----------------------------------------------------------------------------
% 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
