Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: real_fun_props.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.