%-----------------------------------------------------------------------------
% Properties of mapping functions on sequences of countable length.
%
% 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_map_props[T1, T2: TYPE]: THEORY
BEGIN
IMPORTING csequence_nth[T1], csequence_nth[T2]
IMPORTING csequence_codt_map[T1, T2]
t: VAR T1
p: VAR pred[T2]
f: VAR [T1 -> T2]
cseq, cseq1, cseq2: VAR csequence[T1]
fseq: VAR finite_csequence[T1]
iseq: VAR infinite_csequence[T1]
nseq: VAR nonempty_csequence[T1]
nfseq: VAR nonempty_finite_csequence[T1]
map_empty: THEOREM FORALL f, cseq: empty?(map(f, cseq)) IFF empty?(cseq)
map_nonempty: THEOREM
FORALL f, cseq: nonempty?(map(f, cseq)) IFF nonempty?(cseq)
map_finite: JUDGEMENT map(f, fseq) HAS_TYPE finite_csequence[T2]
map_infinite: JUDGEMENT map(f, iseq) HAS_TYPE infinite_csequence[T2]
map_first: THEOREM FORALL f, nseq: first(map(f, nseq)) = f(first(nseq))
map_rest: THEOREM FORALL f, nseq: rest(map(f, nseq)) = map(f, rest(nseq))
map_length: THEOREM FORALL f, fseq: length(map(f, fseq)) = length(fseq)
map_index: THEOREM FORALL f, cseq: index?(map(f, cseq)) = index?(cseq)
map_nth: THEOREM
FORALL f, cseq, (n: indexes(cseq)):
nth(map(f, cseq), n) = f(nth(cseq, n))
map_add: THEOREM
FORALL f, cseq, t: add(f(t), map(f, cseq)) = map(f, add(t, cseq))
map_last: THEOREM FORALL f, nfseq: last(map(f, nfseq)) = f(last(nfseq))
% The generated map theory includes both curried and uncurried definitions
% of map, but doesn't prove that they are equal.
map_map: THEOREM FORALL f, cseq: map(f)(cseq) = map(f, cseq)
map_injective: THEOREM FORALL f: injective?(f) IMPLIES injective?(map(f))
map_extensionality: THEOREM
FORALL f, cseq1, cseq2:
injective?(f) AND map(f, cseq1) = map(f, cseq2) IMPLIES cseq1 = cseq2
map_some: THEOREM
FORALL f, cseq, p: some(p)(map(f, cseq)) IFF some(p o f)(cseq)
map_every: THEOREM
FORALL f, cseq, p: every(p)(map(f, cseq)) IFF every(p o f)(cseq)
END csequence_map_props
¤ 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.
|
