Quelle real_fun_props.pvs Sprache: PVS

real_fun_props [T : TYPE FROM real] : THEORY
%----------------------------------------------------------------------%
%  Defines several properties of functions [T -> real]                 %
%  -> increasing/decreasing functions                                  %
%  -> upper/lower bound                                                %
%  -> maximum/minimum of a function                                    %
%----------------------------------------------------------------------%
BEGIN

  IMPORTING real_fun_ops, real_fun_preds

  f    : VAR [T -> real]
  x, y : VAR T
  a, z : VAR real

  %-------------------
  %  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_neg       : LEMMA increasing?(- f) IFF decreasing?(f)
  decr_neg       : LEMMA decreasing?(- f) IFF increasing?(f)

  strict_incr_neg: LEMMA strict_increasing?(- f) IFF strict_decreasing?(f)
  strict_decr_neg: LEMMA strict_decreasing?(- f) IFF strict_increasing?(f)

  %-----------------------
  %  Constant functions
  %-----------------------

  constant_to_incr    : LEMMA  constant?(f) IMPLIES increasing?(f)
  constant_to_decr    : LEMMA  constant?(f) IMPLIES decreasing?(f)
  constant_neg        : LEMMA  constant?(- f) IFF constant?(f)

  %------------------------
  %  Relation to negative function
  %------------------------

  bounded_above_neg : LEMMA bounded_above?(- f) IFF bounded_below?(f)
  bounded_below_neg : LEMMA bounded_below?(- f) IFF bounded_above?(f)

  %------------------------
  %  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 negative functions
  %----------------------------------

  max_neg : LEMMA  is_maximum?(x, - f) IFF is_minimum?(x, f)
  min_neg : LEMMA  is_minimum?(x, - f) IFF is_maximum?(x, f)

  %--------------------------------------------------------
  %  Image of a function
  %   redefined from function_image to avoid conversions
  %--------------------------------------------------------

  E: VAR setof[real]

  Im(f)    : setof[real] = { z | EXISTS x : z = f(x) }
  Im(f, E) : setof[real] = { z | EXISTS x : E(x) AND z = f(x) }

END real_fun_props

quality93%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.