%------------------------------------------------------------------------------
% Generalized log function (without ln/exp)
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            19/08/08   Initial version (DRL)
%
%------------------------------------------------------------------------------

nn_log: THEORY

BEGIN

  IMPORTING rational_props_aux,
            nn_root,
            nn_rational_expt,
            nnreal_expt

  a,b,x,y,z: VAR nnreal  
  q:       VAR nnrat
  px,py,pa,pb,
  delta,r,
  epsilon:   VAR posreal
  ne1x: VAR {r | r /= 1}
  gt1x,gt1y: VAR {r | r > 1}
  lt1x,lt1y: VAR {r | r < 1}

  log_gt1(gt1x):[{r | r>=1}->nnreal]
    = inverse[nnreal,{r | r>=1}](lambda x: nnreal_expt(gt1x,x))

  log_lt1(lt1x):[{r | r<=1}->nnreal]
    = inverse[nnreal,{r | r<=1}](lambda x: nnreal_expt(lt1x,x))

  nn_log(ne1x)(y:{r | ne1x>1 AND r>=1 OR ne1x<1 AND r<=1}):nnreal
    = IF ne1x>1 THEN log_gt1(ne1x)(y) ELSE log_lt1(ne1x)(y) ENDIF

  nn_log_expt: LEMMA nn_log(ne1x)(nnreal_expt(ne1x,y)) = y
  nn_expt_log: LEMMA FORALL (y:{r | ne1x>1 AND r>=1 OR ne1x<1 AND r<=1}):
                         nnreal_expt(ne1x,nn_log(ne1x)(y)) = y

  nn_log_plus: LEMMA FORALL (x,y:{r | ne1x>1 AND r>=1 OR ne1x<1 AND r<=1}):
                         nn_log(ne1x)(x*y) = nn_log(ne1x)(x) + nn_log(ne1x)(y)

  nn_log_1:    LEMMA nn_log(ne1x)(1)    = 0
  nn_log_ne1x: LEMMA nn_log(ne1x)(ne1x) = 1
  nn_log_gt1:  LEMMA nn_log(gt1x)(gt1y) > 1 IFF gt1y > gt1x

  nn_inv_base_log: LEMMA
     FORALL (y:{r | ne1x>1 AND r<=1 OR ne1x<1 AND r>=1}):
            nn_log(1/ne1x)(y) = nn_log(ne1x)(1/y)


  nn_log_increasing:  LEMMA 1 < x AND x < y =>
                                nn_log(gt1x)(x) < nn_log(gt1x)(y)

END nn_log