%-----------------------------------------------------------------------------
% Functions that generate infinite sequences.
%
% 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_generate[T: TYPE]: THEORY
BEGIN
IMPORTING function_iterate[T], csequence_nth[T]
IMPORTING csequence_codt_coreduce[T, [[T -> T], T]]
n: VAR nat
t, u: VAR T
p: VAR pred[T]
f, g: VAR [T -> T]
state: VAR [[T -> T], T]
% The generator is given a starting T, and a function that generates the
% next T from the previous one.
generate_struct(state): csequence_struct =
inj_add(state`2, (state`1, state`1(state`2)))
generate(f, t): infinite_csequence = coreduce(generate_struct)((f, t))
generate_first: THEOREM FORALL f, t: first(generate(f, t)) = t
generate_rest: THEOREM
FORALL f, t: rest(generate(f, t)) = generate(f, f(t))
generate_nth: THEOREM
FORALL f, t, n: nth(generate(f, t), n) = iterate(f, n)(t)
generate_add: THEOREM
FORALL f, t, u: t = f(u) IMPLIES add(u, generate(f, t)) = generate(f, u)
generate_some: THEOREM
FORALL f, t, p:
some(p)(generate(f, t)) IFF (EXISTS n: p(iterate(f, n)(t)))
generate_every: THEOREM
FORALL f, t, p:
every(p)(generate(f, t)) IFF (FORALL n: p(iterate(f, n)(t)))
END csequence_generate
¤ Dauer der Verarbeitung: 0.16 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.
|
