|
sequence_props : THEORY
%----------------------------------------------------------------------------
% Properties of real sequences %
% -> condition for increasing? / decreasing %
% -> subsequences %
%
% Author: Bruno Dutertre Royal Holloway & Bedford New College
%----------------------------------------------------------------------------
BEGIN
IMPORTING real_fun_supinf
u, v, w : VAR sequence[real]
i, j : VAR nat
a, x : VAR real
n : VAR nat
%--------------------------------------------------
% Conditions for increasing?/decreasing sequences
%--------------------------------------------------
incr_condition : LEMMA increasing?(u) IFF FORALL i : u(i) <= u(i+1)
decr_condition : LEMMA decreasing(u) IFF FORALL i : u(i+1) <= u(i)
strict_incr_condition : LEMMA strict_increasing?(u)
IFF FORALL i : u(i) < u(i+1)
strict_decr_condition : LEMMA strict_decreasing(u)
IFF FORALL i : u(i+1) < u(i)
%-------------------------------------------------------
% Increasing sequences of natural numbers
% used for extracting a sub-sequence from a sequence
%-------------------------------------------------------
extraction : TYPE = { f : [nat -> nat] | strict_increasing?(f) }
f, g : VAR extraction
extract_incr1 : LEMMA f(i) < f(j) IFF i < j
extract_incr2 : LEMMA i <= j IMPLIES f(i) <= f(j)
extract_incr3 : LEMMA i <= f(i)
unbounded_extract1 : LEMMA EXISTS j : i <= f(j)
unbounded_extract2 : LEMMA EXISTS j : i < f(j)
extract_composition : LEMMA strict_increasing?(g o f)
%-----------------
% Sub-sequences
%-----------------
subseq(u, v) : bool = EXISTS f : FORALL i : u(i) = v(f(i))
subseq_def: LEMMA subseq(u,v) IFF EXISTS f: FORALL n: u(n) = v(f(n))
reflexive_subseq : LEMMA subseq(u, u)
transitive_subseq : LEMMA subseq(u, v) AND subseq(v, w) IMPLIES subseq(u, w)
extract_bij: LEMMA bijective?[nat,(image(f,fullset[nat]))](f)
%-----------------------------------------
% Properties inherited by subsequences
%-----------------------------------------
incr_subseq : LEMMA increasing?(v) AND subseq(u, v) IMPLIES increasing?(u)
decr_subseq : LEMMA decreasing(v) AND subseq(u, v) IMPLIES decreasing(u)
strict_incr_subseq : LEMMA strict_increasing?(v) AND subseq(u, v)
IMPLIES strict_increasing?(u)
strict_decr_subseq : LEMMA strict_increasing?(v) AND subseq(u, v)
IMPLIES strict_increasing?(u)
bounded_above_subseq: LEMMA bounded_above?(v) AND subseq(u, v)
IMPLIES bounded_above?(u)
bounded_below_subseq: LEMMA bounded_below?(v) AND subseq(u, v)
IMPLIES bounded_below?(u)
bounded_subseq : LEMMA bounded?(v) AND subseq(u, v) IMPLIES bounded?(u)
END sequence_props
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
