%-----------------------------------------------------------------------------
% Insert an element into a sequence of countable length defined as a
% coalgebraic datatype.
%
% 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_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
