integral_sincos[T : TYPE+ FROM real ] : THEORY
%------------------------------------------------------------------------------
%  Convenient forms of sin cos integrals.
%
%      Rick Butler 4/1/2010
%------------------------------------------------------------------------------
BEGIN
   ASSUMING
     IMPORTING analysis_ax@deriv_domain

     connected_domain: ASSUMPTION connected?[T]

     not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   AUTO_REWRITE+ connected_domain
   AUTO_REWRITE+ not_one_element


   IMPORTING analysis_ax@deriv_domain, deriv_sincos[T], analysis_ax@fundamental_theorem[T]

   k,alpha: VAR real
   a,b: VAR T
  
   sin_Integrable: LEMMA
         Integrable?[T](a, b, LAMBDA (x: T): k * sin(alpha * x))

   cos_Integrable: LEMMA
         Integrable?[T](a, b, LAMBDA (x: T): k * cos(alpha * x))

   Integral_sin: LEMMA alpha /= 0 IMPLIES
         Integral[T](a,b, (LAMBDA (x:T): k*sin(alpha*x))) = -k/alpha*(cos(alpha*b) - cos(alpha*a)) 
 
  
   Integral_cos: LEMMA alpha /= 0 IMPLIES
         Integral[T](a,b, (LAMBDA (x:T): k*cos(alpha*x))) = k/alpha*(sin(alpha*b) - sin(alpha*a))


END integral_sincos