%-----------------------------------------------------------------------------
% Properties of the add operator on sequences of countable length defined as
% coalgebraic datatypes.
%
% 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_add[T: TYPE]: THEORY
BEGIN
IMPORTING csequence_nth[T]
n: VAR nat
t: VAR T
p: VAR pred[T]
cseq: VAR csequence
fseq: VAR finite_csequence
iseq: VAR infinite_csequence
add_finite: JUDGEMENT add(t, fseq) HAS_TYPE nonempty_finite_csequence
add_infinite: JUDGEMENT add(t, iseq) HAS_TYPE infinite_csequence
add_length: THEOREM
FORALL t, fseq: length(add(t, fseq)) = length(fseq) + 1
add_index: THEOREM
FORALL t, cseq, n:
index?(add(t, cseq))(n) IFF n = 0 OR index?(cseq)(n - 1)
add_nth: THEOREM
FORALL t, cseq, (n: indexes(cseq)):
nth(add(t, cseq), n + 1) = nth(cseq, n)
add_last: THEOREM
FORALL t, fseq:
last(add(t, fseq)) = IF empty?(fseq) THEN t ELSE last(fseq) ENDIF
add_some: THEOREM
FORALL t, cseq, p: some(p)(add(t, cseq)) IFF p(t) OR some(p)(cseq)
add_every: THEOREM
FORALL t, cseq, p: every(p)(add(t, cseq)) IFF p(t) AND every(p)(cseq)
END csequence_add
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
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.
|
