Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: hausdorff_convergence.pvs Sprache: PVS

Original von: PVS^©

%-----------------------------------------------------------------------------
% Append an element to a sequence of countable length defined as a coalgebraic
% datatype.  This operation has no effect if the sequence is infinite.
%
% 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_append[T: TYPE]: THEORY
BEGIN

  IMPORTING csequence_insert[T]
  IMPORTING csequence_codt_coreduce[T, [csequence, T, bool]]

  n: VAR nat
  t, u: VAR T
  p: VAR pred[T]
  state: VAR [csequence, T, bool]
  cseq, cseq1, cseq2: VAR csequence
  nseq: VAR nonempty_csequence
  fseq: VAR finite_csequence
  iseq: VAR infinite_csequence

  % The boolean distinguishes between the two cases when the sequence part of
  % the state is empty?: (1) the T has been appended; and (2) the T has not
  % been appended.
  append_struct(state): csequence_struct =
      IF state`3 THEN inj_empty_cseq
      ELSIF empty?(state`1)
        THEN inj_add(state`2, (state`1, state`2, TRUE))
      ELSE inj_add(first(state`1), (rest(state`1), state`2, FALSE))
      ENDIF

  append(t, cseq): nonempty_csequence =
      coreduce(append_struct)(cseq, t, FALSE)

  append_finite: JUDGEMENT append(t, fseq) HAS_TYPE nonempty_finite_csequence

  append_first: THEOREM
    FORALL t, cseq:
      first(append(t, cseq)) = IF empty?(cseq) THEN t ELSE first(cseq) ENDIF

  append_rest: THEOREM
    FORALL t, nseq: rest(append(t, nseq)) = append(t, rest(nseq))

  append_finite_def: THEOREM
    FORALL t, fseq: append(t, fseq) = insert(t, length(fseq), fseq)

  append_infinite_def: THEOREM FORALL t, iseq: append(t, iseq) = iseq

  append_length: THEOREM
    FORALL t, fseq: length(append(t, fseq)) = length(fseq) + 1

  append_index: THEOREM
    FORALL t, cseq, n:
      index?(append(t, cseq))(n) IFF
       (is_finite(cseq) AND n = length(cseq)) OR index?(cseq)(n)

  append_nth: THEOREM
    FORALL t, cseq, (n: indexes(cseq)):
      nth(append(t, cseq), n) = nth(cseq, n)

  append_add: THEOREM
    FORALL t, u, cseq: add(u, append(t, cseq)) = append(t, add(u, cseq))

  append_last: THEOREM FORALL t, fseq: last(append(t, fseq)) = t

  append_extensionality: THEOREM
    FORALL t, cseq1, cseq2:
      append(t, cseq1) = append(t, cseq2) IMPLIES cseq1 = cseq2

  append_some: THEOREM
    FORALL t, cseq, p:
      some(p)(append(t, cseq)) IFF
       some(p)(cseq) OR (is_finite(cseq) AND p(t))

  append_every: THEOREM
    FORALL t, cseq, p:
      every(p)(append(t, cseq)) IFF
       every(p)(cseq) AND (is_infinite(cseq) OR p(t))

END csequence_append

¤ Dauer der Verarbeitung: 0.20 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.