%-----------------------------------------------------------------------------
% Unzip a countable sequence of pairs into a pair of sequences.
%
% 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_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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
