Quelle  csequence_split.pvs

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