derivative_inverse [ T1, T2: TYPE FROM real ]: THEORY
%------------------------------------------------------------------------------
%
% Derivative of Inverse
%
% Author: David Lester (Manchester University)
%
%------------------------------------------------------------------------------
BEGIN

  ASSUMING

     IMPORTING  deriv_domain_def

     connected_domain1 : ASSUMPTION connected?[T1]
 
     not_one_element1  : ASSUMPTION not_one_element?[T1]
 
     connected_domain2 : ASSUMPTION connected?[T2]
 
     not_one_element2  : ASSUMPTION not_one_element?[T2]

  ENDASSUMING

  deriv_domain1: LEMMA deriv_domain?[T1]
  deriv_domain2: LEMMA deriv_domain?[T2]


  IMPORTING derivatives, derivative_props, % derivatives_more,
            chain_rule, inverse_continuous_functions,
            lim_of_functions, composition_continuous


  F: VAR [T1 -> T2]
  G: VAR [T2 -> T1]
  f: VAR [T1 -> nzreal] % WAS: {nzx:nzreal| T2_pred(1/nzx)}]
  x: VAR T2


  inverse_derivable: LEMMA
     derivable?[T1](F) AND bijective?[T1,T2](F) AND deriv[T1](F) = f
     AND inverse?[T1,T2](G,F) IMPLIES derivable?[T2](G,x)

  inverse_derivable_fun: LEMMA
     derivable?[T1](F) AND bijective?[T1,T2](F) AND deriv[T1](F) = f
     AND inverse?[T1,T2](G,F) IMPLIES derivable?[T2](G)

  deriv_inverse_fun: LEMMA derivable?[T1](F) AND deriv[T1](F) = f
     AND bijective?[T1,T2](F) AND inverse?[T1,T2](G,F)
   IMPLIES deriv[T2](G) = (LAMBDA (x:T2): 1/f(G(x)))


  deriv_inverse: LEMMA derivable?[T1](F) AND deriv[T1](F) = f
                       AND bijective?[T1,T2](F) AND inverse?[T1,T2](G,F)
                   IMPLIES derivable?[T1](F) AND 
                           deriv[T2](G) = (LAMBDA (x:T2): 1/f(G(x)))

END derivative_inverse