|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
csequence_append.pvs
Sprache: 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
[ zur Elbe Produktseite wechseln0.17Quellennavigators
Analyse erneut starten
]
|
|
|
|
|
|
