%-----------------------------------------------------------------------------
% Singleton sequences, 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_singleton[T: TYPE]: THEORY
BEGIN
IMPORTING csequence_nth[T]
t: VAR T
p: VAR pred[T]
n: VAR nat
cseq: VAR csequence
singleton_cseq?(cseq): bool = nonempty?(cseq) AND empty?(rest(cseq))
singleton_is_nonempty_finite: JUDGEMENT
(singleton_cseq?) SUBTYPE_OF nonempty_finite_csequence
singleton_cseq_length: THEOREM
FORALL cseq: singleton_cseq?(cseq) IMPLIES length(cseq) = 1
singleton_cseq_index: THEOREM
FORALL (single: (singleton_cseq?)), n: index?(single)(n) IFF n = 0
singleton_cseq(t): (singleton_cseq?) = add(t, empty_cseq)
singleton_def: THEOREM
FORALL cseq:
singleton_cseq?(cseq) IMPLIES cseq = singleton_cseq(first(cseq))
singleton_cseq_first: THEOREM FORALL t: first(singleton_cseq(t)) = t
singleton_cseq_rest: THEOREM FORALL t: rest(singleton_cseq(t)) = empty_cseq
singleton_cseq_last: THEOREM FORALL t: last(singleton_cseq(t)) = t
singleton_cseq_some: THEOREM
FORALL t, p: some(p)(singleton_cseq(t)) IFF p(t)
singleton_cseq_every: THEOREM
FORALL t, p: every(p)(singleton_cseq(t)) IFF p(t)
END csequence_singleton
¤ Dauer der Verarbeitung: 0.1 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.
|
