Quellcode-Bibliothek log.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