Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: ConnectionBuilder.java Sprache: PVS

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

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