derivative_props [ T : TYPE FROM real ] : THEORY
BEGIN

  ASSUMING
     IMPORTING deriv_domain_def

     connected_domain : ASSUMPTION connected?[T]

     not_one_element : ASSUMPTION not_one_element?[T]

  ENDASSUMING

  IMPORTING derivatives_alt[T], continuous_functions_props

%  AUTO_REWRITE-  abs_0
  AUTO_REWRITE-  abs_neg

  deriv_domain: LEMMA deriv_domain?[T]


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

  %--------------------------------------

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


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


  %-----------------------
  %  Mean value theorem
  %-----------------------

  mean_value_aux : LEMMA derivable?(f) AND a < b AND f(a) = f(b) IMPLIES
                           EXISTS c : a < c AND c < b AND deriv(f, c) = 0

  mean_value : THEOREM derivable?(f) AND a < b IMPLIES
                           EXISTS c : a < c AND c < b AND 
                                      deriv(f, c) * (b - a) = f(b) - f(a)


  mean_value_abs : THEOREM derivable?(f) AND a /= b IMPLIES  % BUTLER
                           EXISTS c: min(a,b) < c AND c < max(a,b) AND 
                              abs(deriv(f, c)) * abs(b - a) = abs(f(b) - f(a))


  %------------------------------------------
  %  Applications of the mean value theorem
  %------------------------------------------

  g : VAR deriv_fun[T]

  nonneg_derivative : LEMMA increasing?(g) IFF (FORALL x : deriv(g, x) >= 0)

  nonpos_derivative : LEMMA decreasing?(g) IFF (FORALL x : deriv(g, x) <= 0)

  positive_derivative : LEMMA (FORALL x: deriv(g, x) > 0) 
                                  IMPLIES strict_increasing?(g)

  negative_derivative : LEMMA (FORALL x : deriv(g, x) < 0) 
                                  IMPLIES strict_decreasing?(g)

  null_derivative : LEMMA constant?(g) IFF (FORALL x : deriv(g, x) = 0)

%% --- David Lester Additions ---

  minimum_derivative: LEMMA deriv(g)(x) = 0 AND x /= y AND
                          (FORALL (y:T): y /= x IMPLIES deriv(g)(y)*(y-x) > 0) 
                             IMPLIES g(x) < g(y)

  maximum_derivative: LEMMA deriv(g)(x) = 0 AND x /= y AND
                          (FORALL (y:T): y /= x IMPLIES deriv(g)(y)*(y-x) < 0) 
                             IMPLIES g(y) < g(x)

  strict_minimum_derivative: LEMMA strict_increasing?(deriv(g)) AND 
                                   deriv(g)(x) = 0 AND x /= y
                                      IMPLIES g(x) < g(y)

  strict_maximum_derivative: LEMMA strict_decreasing?(deriv(g)) AND 
                                   deriv(g)(x) = 0 AND x /= y
                                      IMPLIES g(y) < g(x)



  monotonic_antideriv: LEMMA FORALL (a, b: T, f, g: deriv_fun[T]):
    (FORALL (x:T): deriv(f)(x) >= deriv(g)(x)) AND
    a <= b =>
    f(b) - f(a) >= g(b) - g(a)

  derivative_alt : LEMMA FORALL (D: real, ff: [T -> real], x: T):
 convergence(NQ(ff, x), 0, D)
    IFF convergence(LAMBDA  (y: {yy:T|yy/=x}): (ff(y) - ff(x))/(y - x), x, D)

  derivative_fun_alt : LEMMA FORALL (ff, gg: [T -> real]):
 derivable?(ff) AND deriv(ff) = gg
    IFF (FORALL x: convergence(LAMBDA  (y: {yy:T|yy/=x}):
                       (ff(y) - ff(x))/(y - x), x, gg(x)))

  epsi_lt_le: LEMMA (FORALL (epsilon: posreal): x < epsilon) IFF
               (FORALL (epsilon: posreal): x <= epsilon) 


END derivative_props