%-----------------------------------------------------------------------------
% Insert an element into a sequence of countable length defined as a
% coalgebraic datatype.
%
% 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_insert[T: TYPE]: THEORY
BEGIN
IMPORTING csequence_nth[T]
t, u: VAR T
p: VAR pred[T]
index, n, m: VAR nat
cseq, cseq1, cseq2: VAR csequence
fseq: VAR finite_csequence
iseq: VAR infinite_csequence
% Insert t at position index in sequence cseq. If index is greater than
% length(cseq), then t is appended instead.
insert(t, index, cseq): RECURSIVE nonempty_csequence =
IF index = 0 OR empty?(cseq) THEN add(t, cseq)
ELSE add(first(cseq), insert(t, index - 1, rest(cseq)))
ENDIF
MEASURE index
insert_finite: JUDGEMENT
insert(t, index, fseq) HAS_TYPE nonempty_finite_csequence
insert_infinite: JUDGEMENT
insert(t, index, iseq) HAS_TYPE infinite_csequence
insert_first: THEOREM
FORALL t, index, cseq:
first(insert(t, index, cseq)) =
IF index = 0 OR empty?(cseq) THEN t ELSE first(cseq) ENDIF
insert_rest: THEOREM
FORALL t, index, cseq:
rest(insert(t, index, cseq)) =
IF index = 0 OR empty?(cseq) THEN cseq
ELSE insert(t, index - 1, rest(cseq))
ENDIF
insert_length: THEOREM
FORALL fseq, t, index: length(insert(t, index, fseq)) = length(fseq) + 1
insert_index: THEOREM
FORALL t, index, cseq, n:
index?(insert(t, index, cseq))(n) IFF n = 0 OR index?(cseq)(n - 1)
insert_nth: THEOREM
FORALL cseq, t, index, (n: indexes(cseq)):
nth(cseq, n) =
nth(insert(t, index, cseq), n + IF n < index THEN 0 ELSE 1 ENDIF)
insert_0: THEOREM FORALL t, cseq: insert(t, 0, cseq) = add(t, cseq)
insert_add: THEOREM
FORALL t, u, index, cseq:
add(u, insert(t, index, cseq)) = insert(t, index + 1, add(u, cseq))
insert_last: THEOREM
FORALL t, index, fseq:
last(insert(t, index, fseq)) =
IF index?(fseq)(index) THEN last(fseq) ELSE t ENDIF
insert_beyond: THEOREM
FORALL t, index, fseq:
index > length(fseq) IMPLIES
insert(t, index, fseq) = insert(t, length(fseq), fseq)
insert_insert: THEOREM
FORALL t, u, n, m, cseq:
insert(t, n, insert(u, m, cseq)) =
IF is_finite(cseq) AND n > length(cseq) AND m > length(cseq)
THEN insert(u, length(cseq), insert(t, n, cseq))
ELSIF n <= m THEN insert(u, m + 1, insert(t, n, cseq))
ELSE insert(u, m, insert(t, n - 1, cseq))
ENDIF
insert_extensionality: THEOREM
FORALL t, index, cseq1, cseq2:
insert(t, index, cseq1) = insert(t, index, cseq2) IMPLIES
cseq1 = cseq2
insert_some: THEOREM
FORALL t, index, cseq:
some(p)(insert(t, index, cseq)) IFF p(t) OR some(p)(cseq)
insert_every: THEOREM
FORALL t, index, cseq:
every(p)(insert(t, index, cseq)) IFF p(t) AND every(p)(cseq)
END csequence_insert
¤ 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.
|
