%-----------------------------------------------------------------------------
% Properties of mapping functions on sequences of countable length.
%
% 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_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
