%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Defines several properties of functions [T -> real] % % -> increasing/decreasing functions % % -> upper/lower bound % % -> maximum/minimum of a function % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% real_fun_props [T : TYPE FROM real] : THEORY BEGIN IMPORTING real_fun_ops f : VAR [T -> real] x, y : VAR T a, z : VAR real E : VAR setof[real] %--------------------------------------- % Increasing and decreasing functions %--------------------------------------- increasing(f) : bool = FORALL x, y : x <= y IMPLIES f(x) <= f(y) decreasing(f) : bool = FORALL x, y : x <= y IMPLIES f(y) <= f(x) strict_increasing(f) : bool = FORALL x, y : x < y IMPLIES f(x) < f(y) strict_decreasing(f) : bool = FORALL x, y : x < y IMPLIES f(y) < f(x) %------------------- % Easy properties %------------------- strict_incr_to_incr : LEMMA strict_increasing(f) IMPLIES increasing(f) strict_decr_to_decr : LEMMA strict_decreasing(f) IMPLIES decreasing(f) incr_opposite : LEMMA increasing(- f) IFF decreasing(f) decr_opposite : LEMMA decreasing(- f) IFF increasing(f) strict_incr_opposite : LEMMA strict_increasing(- f) IFF strict_decreasing(f) strict_decr_opposite : LEMMA strict_decreasing(- f) IFF strict_increasing(f) %----------------------- % Constant functions %----------------------- constant(f) : bool = FORALL x, y : f(x) = f(y) constant_to_incr : LEMMA constant(f) IMPLIES increasing(f) constant_to_decr : LEMMA constant(f) IMPLIES decreasing(f) constant_opposite : LEMMA constant(- f) IFF constant(f) %-------------------------------------------------------- % Image of a function % redefined from function_image to avoid conversions %-------------------------------------------------------- Im(f) : setof[real] = { z | EXISTS x : z = f(x) } Im(f, E) : setof[real] = { z | EXISTS x : E(x) AND z = f(x) } %--------------------- % Bounded functions %--------------------- bounded_above?(f) : bool = EXISTS a: FORALL x: f(x) <= a bounded_below?(f) : bool = EXISTS a: FORALL x: a <= f(x) bounded?(f) : bool = bounded_above?(f) AND bounded_below?(f) %------------------------ % Relation to opposite %------------------------ bounded_above_opposite : LEMMA bounded_above?(- f) IFF bounded_below?(f) bounded_below_opposite : LEMMA bounded_below?(- f) IFF bounded_above?(f) %----------------------------------- % Maximum / minimum of a function %----------------------------------- is_maximum(x, f) : bool = FORALL y : f(y) <= f(x) is_minimum(x, f) : bool = FORALL y : f(x) <= f(y) %------------------------ % Relation with bounds %------------------------ max_bounded : LEMMA is_maximum(x, f) IMPLIES bounded_above?(f) min_bounded : LEMMA is_minimum(x, f) IMPLIES bounded_below?(f) %--------------------------- % Relation with opposites %--------------------------- max_opposite : LEMMA is_maximum(x, - f) IFF is_minimum(x, f) min_opposite : LEMMA is_minimum(x, - f) IFF is_maximum(x, f) END real_fun_props