table_of_integrals[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------
%
%  New experimental:  Theorems will be added as they are needed
%
%  Author:  Rick Butler               NASA Langley
%------------------------------------------------------------------------------

BEGIN

   ASSUMING
      IMPORTING deriv_domain_def[T]

      connected_domain : ASSUMPTION connected?[T]

      not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   IMPORTING fundamental_theorem[T], indefinite_integral[T]

   a,b,x: VAR T

%  ------ Integral c x^n  = (c/(n+1))*x^(n+1) -----

   antideriv_x_to_n: LEMMA FORALL (n: posnat, c: real):
                            LET f = (LAMBDA x: c*x^n),
                                F = (LAMBDA x: (c/(n+1))*x^(n+1)) IN
                            antiderivative?(F,f)


   integral_x_to_n: LEMMA FORALL (n: posnat, c: real):
                            LET f = (LAMBDA x: c*x^n) IN
                            Integrable?(a,b,f) AND 
                         LET F = (LAMBDA x: (c/(n+1))*x^(n+1)) IN
                     Integral(a,b,f) = F(b) - F(a)

   integral_linear: LEMMA FORALL (mm: real, bb: real):
                            LET f = (LAMBDA x: mm*x+bb) IN
                            Integrable?(a,b,f) AND 
                         LET F = (LAMBDA x: (mm/2)*x^2 +bb*x) IN
                     Integral(a,b,f) = F(b) - F(a)

   integral_quadratic: LEMMA FORALL (A,B,C: real):
                       Integrable?(a,b, LAMBDA x: A*x^2+B*x+C) AND 
                       LET F =(LAMBDA x: (A/3)*x^3 +(B/2)*x^2 +C*x) IN
                       Integral(a,b, LAMBDA x: A*x^2+B*x+C) = F(b)-F(a)

%  -------

%   IMPORTING sqrt_derivative

%   integral_a_to_x: LEMMA LET f = (LAMBDA x: a^^x) IN
%                              Integrable?(a,b,f) AND 
%                              Integral(a,b,f) = F(b) - F(a)

%   integral_1_div_sqrt: LEMMA LET f = (LAMBDA (t: nnreal): 1/sqrt(t)) IN
%                           a > 0 AND b > 0 IMPLIES  
%                         Integrable?(a,b,f) AND
%                         Integral(a, b, f)  = 2*sqrt(b) - 2*sqrt(a)



END table_of_integrals