%-----------------------------------------------------------------------------
% Functions that generate sequences until a limit condition is met.
%
% 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_limit[T: TYPE]: THEORY
BEGIN
IMPORTING function_iterate[T], csequence_nth[T]
IMPORTING csequence_codt_coreduce[T, [[T -> T], T, pred[T]]]
t, u: VAR T
p: VAR pred[T]
f: VAR [T -> T]
n: VAR nat
stop?: VAR pred[T]
state: VAR [[T -> T], T, pred[T]]
% The sequence generated from a generator function, a starting element, and
% a predicate that determines when the next T should not appear in the
% sequence.
generate_limit_struct(state): csequence_struct =
IF state`3(state`2) THEN inj_empty_cseq
ELSE inj_add(state`2, (state`1, state`1(state`2), state`3))
ENDIF
generate(f, t, stop?): csequence =
coreduce(generate_limit_struct)((f, t, stop?))
generate_empty: THEOREM
FORALL f, t, stop?: empty?(generate(f, t, stop?)) IFF stop?(t)
generate_first: THEOREM
FORALL f, t, stop?: stop?(t) OR first(generate(f, t, stop?)) = t
generate_rest: THEOREM
FORALL f, t, stop?:
stop?(t) OR rest(generate(f, t, stop?)) = generate(f, f(t), stop?)
% This lemma is helpful in proving the next theorem
generate_has_length: LEMMA
FORALL f, t, stop?, n:
has_length(generate(f, t, stop?), n) IFF
(stop?(iterate(f, n)(t)) AND
(FORALL (m: below[n]): NOT stop?(iterate(f, m)(t))))
generate_finite: THEOREM
FORALL f, t, stop?:
is_finite(generate(f, t, stop?)) IFF (EXISTS n: stop?(iterate(f, n)(t)))
generate_nth: THEOREM
FORALL f, t, stop?, (n: indexes(generate(f, t, stop?))):
nth(generate(f, t, stop?), n) = iterate(f, n)(t)
generate_add: THEOREM
FORALL f, t, stop?, u:
t = f(u) AND NOT stop?(u) IMPLIES
add(u, generate(f, t, stop?)) = generate(f, u, stop?)
generate_some: THEOREM
FORALL f, t, stop?, p:
some(p)(generate(f, t, stop?)) IFF
(EXISTS (n: indexes(generate(f, t, stop?))): p(iterate(f, n)(t)))
generate_every: THEOREM
FORALL f, t, stop?, p:
every(p)(generate(f, t, stop?)) IFF
(FORALL (n: indexes(generate(f, t, stop?))): p(iterate(f, n)(t)))
END csequence_generate_limit
¤ 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.
|
