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

nn_rational_expt: THEORY

BEGIN

  IMPORTING rational_props_aux,
            nn_root

  x,y,z,x1,x2: VAR nnreal  
  px,py,epsilon,delta:   VAR posreal
  q,r:     VAR nnrat
  pq:      VAR posrat
  n:       VAR nat
  pn:      VAR posnat

  nn_rational_expt(x,q):nnreal = nn_root(expt(x,numerator(q)),denominator(q))

  nn_rational_expt_nat_rew:  LEMMA nn_rational_expt(x,n)    = x^n
  nn_rational_expt_root_rew: LEMMA nn_rational_expt(x,1/pn) = nn_root(x,pn)
  nn_rational_expt_rat_rew:  LEMMA nn_rational_expt(x,n/pn) = nn_root(x^n,pn)

  nn_rational_expt_strict_increasing: LEMMA x < y =>
                               nn_rational_expt(x,pq) <  nn_rational_expt(y,pq)

  nn_rational_expt_0q: LEMMA nn_rational_expt(0,q)
                              = IF q = 0 THEN 1 ELSE 0 ENDIF
  nn_rational_expt_1q: LEMMA nn_rational_expt(1,q) = 1
  nn_rational_expt_x1: LEMMA nn_rational_expt(x,1) = x

  nn_rational_expt_is_0: LEMMA nn_rational_expt(x,q) = 0 IFF x = 0 AND q /= 0
  nn_rational_expt_pos:  LEMMA nn_rational_expt(px,q) > 0
  nn_rational_expt_gt1:  LEMMA nn_rational_expt(x,pq) > 1 IFF x > 1
  nn_rational_expt_lt1:  LEMMA nn_rational_expt(x,pq) < 1 IFF x < 1

  mult_nn_rational_expt: LEMMA nn_rational_expt(x*y,q)
                               = nn_rational_expt(x,q)*nn_rational_expt(y,q)
  inv_nn_rational_expt:  LEMMA nn_rational_expt(1/px,q)
                               = 1/nn_rational_expt(px,q)
  div_nn_rational_expt:  LEMMA nn_rational_expt(x/py,q)
                               = nn_rational_expt(x,q)/nn_rational_expt(py,q)

  nn_rational_expt_plus: LEMMA nn_rational_expt(x,q+r)
                               = nn_rational_expt(x,q)*nn_rational_expt(x,r)
  nn_rational_expt_times:LEMMA nn_rational_expt(x,q*r)
                               = nn_rational_expt(nn_rational_expt(x,q),r)

  nn_rational_expt_decreasing: LEMMA q < r AND 0 < x AND x < 1 =>
                             nn_rational_expt(x,q) > nn_rational_expt(x,r)

  nn_rational_expt_increasing: LEMMA q < r AND 1 < x =>
                             nn_rational_expt(x,q) < nn_rational_expt(x,r)

  nn_rational_expt_def: LEMMA
       nn_rational_expt(x,q) = expt(nn_root(x,denominator(q)),numerator(q))

  continuous_alt_nn_rational_expt: LEMMA
     EXISTS delta: FORALL x2: abs(x1-x2) < delta
                => abs(nn_rational_expt(x1,q)-nn_rational_expt(x2,q)) < epsilon

  nn_rational_expt_approx_gt1: LEMMA
     x > 1 AND y > 1 => EXISTS q: abs(nn_rational_expt(x,q)-y) < epsilon

END nn_rational_expt