Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: sigma_lemmas.pvs Sprache: PVS

Original von: PVS^©

%-----------------------------------------------------------------------------
% Conversions between sequences of countable length and the prelude sequence
% type.
%
% 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_sequence[T: TYPE]: THEORY
BEGIN

  IMPORTING sequences[T], csequence_nth[T]
  IMPORTING csequence_codt_coreduce[T, sequence]

  n: VAR nat
  seq: VAR sequence
  iseq: VAR infinite_csequence

  % Convert a sequence to an infinite_csequence
  from_sequence_struct(seq): csequence_struct =
      inj_add(seq(0), LAMBDA n: seq(1 + n))

  from_sequence(seq): infinite_csequence =
      coreduce(from_sequence_struct)(seq)

  from_sequence_nth: THEOREM
    FORALL seq, n: nth(from_sequence(seq), n) = seq(n)

  % Convert an infinite_csequence to a sequence
  to_sequence(iseq): sequence = LAMBDA n: nth(iseq, n)

  to_sequence_nth: THEOREM
    FORALL iseq, n: to_sequence(iseq)(n) = nth(iseq, n)

  % Applying both conversions gives you back what you started with

  to_from_sequence: THEOREM
    FORALL seq: to_sequence(from_sequence(seq)) = seq

  from_to_sequence: THEOREM
    FORALL iseq: from_sequence(to_sequence(iseq)) = iseq

END csequence_sequence

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