Quelle log.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Generalized log function (without ln/exp)
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            19/08/08   Initial version (DRL)
%
% If we had ln to hand, then we could define
%
%   log(x)(y) = ln(y)/ln(x)
%
% Of course that would defeat the whole point of this library,
% which is to be independent of the definition of ln/exp.
%
%------------------------------------------------------------------------------

log: THEORY

BEGIN

  IMPORTING nn_log,
            real_expt

  a,b,r,x,y: VAR posreal
  z:         VAR real
  i:         VAR int
  ne1x,ne1y,ne1z: VAR {r | r /= 1}
  gt1x,gt1y,gt1z: VAR {r | r > 1}
  lt1x,lt1y,lt1z: VAR {r | r < 1}

  log(ne1x)(y):real
    = IF ne1x > 1 AND y >= 1 OR ne1x < 1 AND y <= 1
      THEN nn_log(ne1x)(y) ELSE -nn_log(ne1x)(1/y) ENDIF

  log(ne1x,y):real = log(ne1x)(y)

  log_expt: LEMMA log(ne1x)(ne1x^z) = z
  expt_log: LEMMA ne1x^log(ne1x)(y) = y

  log_1:        LEMMA log(ne1x)(1)    = 0
  log_ne1x:     LEMMA log(ne1x)(ne1x) = 1
  inv_base_log: LEMMA log(1/ne1x)(y)  = log(ne1x)(1/y)

  log_inv:  LEMMA log(ne1x)(1/y) = -log(ne1x)(y)
  log_mult: LEMMA log(ne1x)(x*y) = log(ne1x)(x) + log(ne1x)(y)
  log_div:  LEMMA log(ne1x)(x/y) = log(ne1x)(x) - log(ne1x)(y)
  log_xz:   LEMMA log(ne1x)(x^z) = z*log(ne1x)(x)

  log_increasing:  LEMMA x < y => log(gt1x)(x) < log(gt1x)(y)
  log_decreasing:  LEMMA x < y => log(lt1x)(x) > log(lt1x)(y)

  log_is_0: LEMMA log(ne1x)(y) = 0 IFF y = 1
  log_pos:  LEMMA log(ne1x)(y) > 0 IFF ne1x>1 AND y>1 OR ne1x<1 AND y<1
  log_neg:  LEMMA log(ne1x)(y) < 0 IFF ne1x>1 AND y<1 OR ne1x<1 AND y>1

  log_increasing1: LEMMA ((ne1z<1 AND (ne1x>1 OR  ne1y<1)) OR
                              (ne1z>1 AND  ne1x<1 AND ne1y>1)) AND
                             ne1x < ne1y =>
                             log(ne1x)(ne1z) < log(ne1y)(ne1z)
  log_decreasing1: LEMMA ((ne1z<1 AND  ne1x<1 AND  ne1y>1)   OR
                              (ne1z>1 AND (ne1x>1 OR   ne1y<1))) AND
                             ne1x < ne1y =>
                             log(ne1x)(ne1z) > log(ne1y)(ne1z)

  both_sides_log_gt1_lt: LEMMA
    log(gt1x)(x) <  log(gt1x)(y) IFF x <  y
  both_sides_log_gt1_le: LEMMA
    log(gt1x)(x) <= log(gt1x)(y) IFF x <= y
  both_sides_log_gt1_gt: LEMMA
    log(gt1x)(x) >  log(gt1x)(y) IFF x >  y
  both_sides_log_gt1_ge: LEMMA
    log(gt1x)(x) >= log(gt1x)(y) IFF x >= y

  both_sides_log_lt1_lt: LEMMA
    log(lt1x)(x) <  log(lt1x)(y) IFF y <  x
  both_sides_log_lt1_le: LEMMA
    log(lt1x)(x) <= log(lt1x)(y) IFF y <= x
  both_sides_log_lt1_gt: LEMMA
    log(lt1x)(x) >  log(lt1x)(y) IFF y >  x
  both_sides_log_lt1_ge: LEMMA
    log(lt1x)(x) >= log(lt1x)(y) IFF y >= x

  both_sides_log: LEMMA log(ne1x)(x) = log(ne1x)(y) IFF x = y

END log

quality100%

¤ Dauer der Verarbeitung: 0.10 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.