%-----------------------------------------------------------------------------
% Unzip a countable sequence of pairs into a pair of sequences.
%
% 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_unzip[T1, T2:
TYPE]:
THEORY
BEGIN
IMPORTING csequence_nth[T1], csequence_nth[T2], csequence_nth[[T1, T2]]
IMPORTING csequence_codt_coreduce[T1, csequence[[T1, T2]]]
IMPORTING csequence_codt_coreduce[T2, csequence[[T1, T2]]]
IMPORTING csequence_codt_map[[T1, T2], T1]
IMPORTING csequence_codt_map[[T1, T2], T2]
n:
VAR nat
t12:
VAR [T1, T2]
p1:
VAR pred[T1]
p2:
VAR pred[T2]
cseq, cseq1, cseq2:
VAR csequence[[T1, T2]]
fseq:
VAR finite_csequence[[T1, T2]]
iseq:
VAR infinite_csequence[[T1, T2]]
nseq:
VAR nonempty_csequence[[T1, T2]]
nfseq:
VAR nonempty_finite_csequence[[T1, T2]]
unzip_left_struct(cseq): csequence_struct[T1, csequence[[T1, T2]]] =
IF empty?(cseq)
THEN inj_empty_cseq
ELSE inj_add(first(cseq)`1, rest(cseq))
ENDIF
unzip_right_struct(cseq): csequence_struct[T2, csequence[[T1, T2]]] =
IF empty?(cseq)
THEN inj_empty_cseq
ELSE inj_add(first(cseq)`2, rest(cseq))
ENDIF
unzip(cseq): [csequence[T1], csequence[T2]] =
(coreduce(unzip_left_struct)(cseq),
coreduce(unzip_right_struct)(cseq))
unzip_finite:
JUDGEMENT
unzip(fseq) HAS_TYPE [finite_csequence[T1], finite_csequence[T2]]
unzip_infinite:
JUDGEMENT
unzip(iseq) HAS_TYPE [infinite_csequence[T1], infinite_csequence[T2]]
unzip_nonempty:
JUDGEMENT
unzip(nseq) HAS_TYPE [nonempty_csequence[T1], nonempty_csequence[T2]]
unzip_empty_left:
THEOREM
FORALL cseq: empty?(unzip(cseq)`1)
IFF empty?(cseq)
unzip_empty_right:
THEOREM
FORALL cseq: empty?(unzip(cseq)`2)
IFF empty?(cseq)
unzip_first_left:
THEOREM
FORALL nseq: first(unzip(nseq)`1) = first(nseq)`1
unzip_first_right:
THEOREM
FORALL nseq: first(unzip(nseq)`2) = first(nseq)`2
unzip_rest_left:
THEOREM
FORALL nseq: rest(unzip(nseq)`1) = unzip(rest(nseq))`1
unzip_rest_right:
THEOREM
FORALL nseq: rest(unzip(nseq)`2) = unzip(rest(nseq))`2
unzip_length_left:
THEOREM
FORALL fseq: length(unzip(fseq)`1) = length(fseq)
unzip_length_right:
THEOREM
FORALL fseq: length(unzip(fseq)`2) = length(fseq)
unzip_index_left:
THEOREM
FORALL cseq, n: index?(unzip(cseq)`1)(n)
IFF index?(cseq)(n)
unzip_index_right:
THEOREM
FORALL cseq, n: index?(unzip(cseq)`2)(n)
IFF index?(cseq)(n)
unzip_nth_left:
THEOREM
FORALL cseq, (n: indexes(cseq)): nth(unzip(cseq)`1, n) = nth(cseq, n)`1
unzip_nth_right:
THEOREM
FORALL cseq, (n: indexes(cseq)): nth(unzip(cseq)`2, n) = nth(cseq, n)`2
unzip_map:
THEOREM
FORALL cseq:
unzip(cseq) =
(map[[T1, T2], T1](PROJ_1, cseq), map[[T1, T2], T2](PROJ_2, cseq))
unzip_extensionality:
THEOREM
FORALL cseq1, cseq2: unzip(cseq1) = unzip(cseq2)
IMPLIES cseq1 = cseq2
unzip_add:
THEOREM
FORALL cseq, t12:
unzip(add(t12, cseq)) =
(add(t12`1, unzip(cseq)`1), add(t12`2, unzip(cseq)`2))
unzip_last_left:
THEOREM
FORALL nfseq: last(unzip(nfseq)`1) = last(nfseq)`1
unzip_last_right:
THEOREM
FORALL nfseq: last(unzip(nfseq)`2) = last(nfseq)`2
unzip_some:
THEOREM
FORALL cseq, p1, p2:
some(p1)(unzip(cseq)`1)
OR some(p2)(unzip(cseq)`2)
IFF
some(
LAMBDA t12: p1(t12`1)
OR p2(t12`2))(cseq)
unzip_every:
THEOREM
FORALL cseq, p1, p2:
every(p1)(unzip(cseq)`1)
AND every(p2)(unzip(cseq)`2)
IFF
every(
LAMBDA t12: p1(t12`1)
AND p2(t12`2))(cseq)
END csequence_unzip
