derivatives_alt [ T : TYPE FROM real ] : THEORY
BEGIN

  ASSUMING

    IMPORTING deriv_domain_def

    deriv_domain     : ASSUMPTION deriv_domain?[T]

    not_one_element : ASSUMPTION not_one_element?[T]

  ENDASSUMING

  IMPORTING derivatives, continuous_functions_props

  AUTO_REWRITE-  abs_neg




  f, fp : VAR [T -> real]
  x, y, a, b, c : VAR T
  D : VAR real


  %--------------------------------------------
  %  Equivalent definitions of differentiation
  %--------------------------------------------

  derivative_equivalence1 : LEMMA (derivable?(f, x) AND deriv(f, x) = D) 
                                    IFF convergence(NQ(f, x), 0, D)

  derivative_equivalence2 : LEMMA convergence(NQ(f, x), 0, D)
                     IFF (EXISTS (phi : [T -> real]) : convergence(phi, x, 0)
                         AND FORALL y : f(y) - f(x) = (y - x) * (D + phi(y)))


  derivative_equivalence3 : LEMMA (derivable?(f,x) AND deriv(f,x) = D) %% Lester
                      IFF (EXISTS (psi : [T -> real]) : convergence(psi, x, D)
                             AND FORALL y : f(y) - f(x) = (y - x) * psi(y))

  epsi_eq_0: LEMMA (FORALL (epsi: posreal): abs(x) < epsi) IFF x = 0

  derivative_squeeze      : LEMMA convergence(NQ(f, x), 0, fp(x))    %% Butler
                                  IFF  (EXISTS (HH: [(A(x)) -> real]): 
                                        convergence(HH,0,0) AND
                               HH = (LAMBDA (h: (A(x))): (NQ(f,x)(h) - fp(x))))


  derivative_squeeze_delta: LEMMA convergence(NQ(f, x), 0, fp(x))    %% Butler
                                  IFF (EXISTS (HH: [(A(x)) -> real]): 
                                      convergence(HH,0,0) AND 
                                      (EXISTS (delta: posreal):
                                  (FORALL (h: (A(x))): (abs(h) < delta) IMPLIES
                                           abs(NQ(f,x)(h) - fp(x)) <= HH(h))))
          

  %------------------------------------
  %  f constant on [a, b]
  %------------------------------------

  deriv_constant1 : LEMMA a < c AND c < b AND 
                          (FORALL x : a < x AND x < b IMPLIES f(x) = f(c))
                              IMPLIES convergence(NQ(f, c), 0, 0)

  deriv_constant2 : LEMMA a < c AND c < b AND 
                          (FORALL x : a < x AND x < b IMPLIES f(x) = f(c))
                              IMPLIES derivable?(f, c) AND deriv(f, c) = 0


END derivatives_alt