root: THEORY

% Computes nth root %

% Narkawicz 12/13 %

BEGIN


  r,x,y: VAR real
  n: VAR posnat
  epsil,delta: VAR posreal
  f,g : VAR [real->real]
  nnr,nnx: VAR nnreal
  m : VAR nat

  mult_expt_pos: LEMMA
    (x*y)^n = x^n*y^n

  real_mult_cont: LEMMA
    (FORALL (epsil,x): EXISTS (delta): FORALL (y):
      abs(x-y)<delta IMPLIES abs(f(x)-f(y))<epsil) AND
    (FORALL (epsil,x): EXISTS (delta): FORALL (y):
      abs(x-y)<delta IMPLIES abs(g(x)-g(y))<epsil)
    IMPLIES
    (FORALL (epsil,x): EXISTS (delta): FORALL (y):
      abs(x-y)<delta IMPLIES abs(f(x)*g(x)-f(y)*g(y))<epsil)
  
  expt_increasing: LEMMA
    nnr<=nnx IMPLIES nnr^m<=nnx^m

  expt_cont: LEMMA
    EXISTS (delta): FORALL (y):
      abs(x-y)<=delta IMPLIES abs(x^n-y^n)<epsil

  nn_root_exists: LEMMA
    EXISTS (nnx): nnx^n=nnr

  root_pos(nnr,n): {nnx|nnx^n=nnr}

  root_real(r)(n|r>=0 OR odd?(n)): {x | (x=0 IFF r = 0) AND
                      (x>0 IFF r>0) AND
      (x<0 IFF r<0) AND
      (x>=0 IFF r>=0) AND
      (x<=0 IFF r<=0) AND
      x^n = r}
    = IF r=0 THEN 0
      ELSIF r>0 THEN root_pos(r,n)
      ELSE -1*root_pos(-r,n) ENDIF


END root