%------------------------------------------------------------------------------
% Power function nnx^nny
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            19/08/08   Initial version (DRL)
%------------------------------------------------------------------------------

nnreal_expt: THEORY

BEGIN

  IMPORTING rational_props_aux,
            nn_root,
            nn_rational_expt

  n:         VAR nat
  pn:        VAR posnat
  a,b,x,y,z: VAR nnreal  
  q:         VAR nnrat
  px,py,pa,pb,
  delta,r,
  epsilon:   VAR posreal

  nnreal_expt(x,y):nnreal
   = IF y = 0 OR x = 1 THEN 1
     ELSIF x < 1 THEN glb({z | EXISTS q: q <= y AND z = nn_rational_expt(x,q)})
                 ELSE lub({z | EXISTS q: q <= y AND z = nn_rational_expt(x,q)})
     ENDIF

  nnreal_expt_rat_rew:  LEMMA nnreal_expt(x,q)    = nn_rational_expt(x,q)
  nnreal_expt_nat_rew:  LEMMA nnreal_expt(x,n)    = x^n
  nnreal_expt_root_rew: LEMMA nnreal_expt(x,1/pn) = nn_root(x,pn)

  nnreal_expt_0a:   LEMMA nnreal_expt(0,a) = IF a = 0 THEN 1 ELSE 0 ENDIF
  nnreal_expt_1a:   LEMMA nnreal_expt(1,a) = 1
  nnreal_expt_x1:   LEMMA nnreal_expt(x,1)  = x

  nnreal_expt_pos:  LEMMA nnreal_expt(px,a) > 0
  nnreal_expt_is_0: LEMMA nnreal_expt(x,a) = 0 IFF x = 0 AND a /= 0
  nnreal_expt_gt1:  LEMMA nnreal_expt(x,pa) > 1 IFF x > 1
  nnreal_expt_lt1:  LEMMA nnreal_expt(x,pa) < 1 IFF x < 1

  inv_nnreal_expt:  LEMMA nnreal_expt(1/px,a) = 1/nnreal_expt(px,a)
  mult_nnreal_expt: LEMMA nnreal_expt(x*y,a)
                               = nnreal_expt(x,a)*nnreal_expt(y,a)
  div_nnreal_expt:  LEMMA nnreal_expt(x/py,a)
                               = nnreal_expt(x,a)/nnreal_expt(py,a)

  nnreal_expt_decreasing: LEMMA a < b AND 0 < x AND x < 1 =>
                                nnreal_expt(x,a) > nnreal_expt(x,b)

  nnreal_expt_increasing: LEMMA a < b AND 1 < x =>
                                nnreal_expt(x,a) < nnreal_expt(x,b)

  nnreal_expt_strict_increasing: LEMMA x < y =>
                                       nnreal_expt(x,pa) < nnreal_expt(y,pa)

  continuous_alt_nnreal_expt2: LEMMA
     EXISTS delta: FORALL pb: abs(pa-pb) < delta
                 => abs(nnreal_expt(x,pa)-nnreal_expt(x,pb)) < epsilon

  ne1x: VAR {r | r /= 1}
  gt1x: VAR {r | r > 1}
  lt1x: VAR {r | r < 1}

  nnreal_bijective1: LEMMA 
     bijective?[nnreal,{r | r>=1}](lambda y: nnreal_expt(gt1x,y))

  nnreal_bijective2: LEMMA
     bijective?[nnreal,{r | r<=1}](lambda y: nnreal_expt(lt1x,y))

  nnreal_expt_def_gt1: LEMMA
     nnreal_expt(gt1x,py)
          = lub({z | EXISTS q: q < py AND z = nn_rational_expt(gt1x,q)})

  nnreal_expt_plus: LEMMA nnreal_expt(x,a+b)= nnreal_expt(x,a)*nnreal_expt(x,b)
  nnreal_expt_times: LEMMA nnreal_expt(x,a*b) = nnreal_expt(nnreal_expt(x,a),b)

END nnreal_expt