derivatives_lam[T: TYPE FROM real ]: THEORY
%------------------------------------------------------------------------------ 
% This theory has been created to support auto-rewriting, e.g.
%
%    auto-rewrite-theory "derivatives_lam[T]"
%
% or via special strategies
%------------------------------------------------------------------------------ 
BEGIN

  ASSUMING

    IMPORTING deriv_domain_def

    deriv_domain     : ASSUMPTION deriv_domain?[T]

    not_one_element  : ASSUMPTION not_one_element?[T]

  ENDASSUMING

  IMPORTING derivatives[T],
            reals@sq


  t   : VAR T
  a   : VAR real
  b   : VAR nzreal
  n   : VAR nat
  m   : VAR posnat
  f,g : VAR deriv_fun
  k   : VAR nz_deriv_fun

  derivable_id_lam     : LEMMA derivable?(LAMBDA(t):t)
  derivable_const_lam  : LEMMA derivable?(LAMBDA(t):a)
  derivable_add_lam    : LEMMA derivable?(LAMBDA(t):f(t)+g(t))
  derivable_mult_lam   : LEMMA derivable?(LAMBDA(t):f(t)*g(t))
  derivable_pow_lam    : LEMMA derivable?(LAMBDA(t):t^n)
  derivable_scal1_lam  : LEMMA derivable?(LAMBDA(t): a*f(t))
  derivable_scal2_lam  : LEMMA derivable?(LAMBDA(t): f(t)*a)
  derivable_neg_lam    : LEMMA derivable?(LAMBDA(t):-g(t))
  derivable_sub_lam    : LEMMA derivable?(LAMBDA(t):f(t)-g(t))
  derivable_sq_lam     : LEMMA derivable?(LAMBDA(t):sq(t))
  derivable_div_lam    : LEMMA derivable?(LAMBDA(t):f(t)/k(t))
  derivable_scald1_lam : LEMMA derivable?(LAMBDA(t): a/k(t))
  derivable_scald2_lam : LEMMA derivable?(LAMBDA(t): f(t)/b)

  deriv_id_lam         : LEMMA deriv(LAMBDA(t):t) = LAMBDA(t):1
      
  deriv_const_lam      : LEMMA deriv(LAMBDA(t):a) = LAMBDA(t):0
       
  deriv_add_lam        : LEMMA deriv(LAMBDA(t):f(t)+g(t)) = LAMBDA(t): deriv(f)(t) + deriv(g)(t)
      
  deriv_mult_lam       : LEMMA deriv(LAMBDA(t):f(t)*g(t)) 
                                 = LAMBDA(t):deriv(f)(t)*g(t) + deriv(g)(t)*f(t)

  deriv_pow_lam        : LEMMA deriv(LAMBDA(t):t^m) = LAMBDA(t):(m*t^(m-1))

  deriv_scal1_lam      : LEMMA deriv(LAMBDA(t): a*f(t)) = LAMBDA(t):a*deriv(f)(t)

  deriv_scal2_lam      : LEMMA deriv(LAMBDA(t): f(t)*a) = LAMBDA(t):a*deriv(f)(t)

  deriv_neg_lam        : LEMMA deriv(LAMBDA(t):-g(t)) = LAMBDA(t):-deriv(g)(t)

  deriv_sub_lam        : LEMMA deriv(LAMBDA(t):f(t)-g(t)) = LAMBDA(t):deriv(f)(t)-deriv(g)(t)

  deriv_sq_lam         : LEMMA deriv(LAMBDA(t):sq(t)) = LAMBDA(t):2*t

  deriv_div_lam        : LEMMA deriv(LAMBDA(t):f(t)/k(t)) 
                                  = LAMBDA(t):(deriv(f)(t)*k(t) - deriv(k)(t)*f(t)) / sq(k(t))

  deriv_scald1_lam     : LEMMA deriv(LAMBDA(t): a/k(t)) 
                                  = LAMBDA(t):-a*deriv(k)(t)/sq(k(t))

  deriv_scald2_lam     : LEMMA deriv(LAMBDA(t): f(t)/b) = LAMBDA(t):(deriv(f)(t))/b

END derivatives_lam