%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Properties of real sequences % % -> condition for increasing / decreasing % % -> subsequences % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% sequence_props : THEORY BEGIN IMPORTING real_fun_supinf u, v, w : VAR sequence[real] i, j : VAR nat a, x : VAR real %-------------------------------------------------- % 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)) reflexive_subseq : LEMMA subseq(u, u) transitive_subseq : LEMMA subseq(u, v) AND subseq(v, w) IMPLIES subseq(u, w) %----------------------------------------- % 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