Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: csequence_unzip.pvs Sprache: PVS

Original von: PVS^©

%-----------------------------------------------------------------------------
% 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.13 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.