Quelle  indefinite_integral.pvs   Sprache: unbekannt

indefinite_integral[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------
%
%  Author:  Rick Butler               NASA Langley
%
%  convention:
%       Definite integral  :  Integral(a,b,f)
%       Indefinite integral:  integral(f)
%
%------------------------------------------------------------------------------

BEGIN

   ASSUMING
      IMPORTING deriv_domain_def[T]

      connected_domain : ASSUMPTION connected?[T]


      not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   deriv_domain: LEMMA deriv_domain?[T]
   IMPORTING integral[T], derivative_props[T]

   a,b,c,x: VAR T
   f,g,F,G,H: VAR [T -> real]

   antiderivative?(F,f): bool = derivable?(F) AND deriv(F) = f


   antiderivative_lem: LEMMA antiderivative?(F,f) AND derivable?(G) AND
                             deriv(G) = f
                             IMPLIES (EXISTS (c: real): F = G + const_fun(c))

   derivs_eq:     THEOREM derivable?(F) AND derivable?(G) AND deriv(F) = deriv(G)
                         IMPLIES (EXISTS (c: real): F = G + const_fun(c))


   % ------ indefinite integral defined over continuous functions ------

   integrable?(f): bool = (EXISTS F: antiderivative?(F,f))

   integrable_fun: TYPE = { f | integrable?(f)}

   IMPORTING fundamental_theorem[T]


   cont_fun_integrable?: LEMMA continuous?(f) IMPLIES integrable?(f)


   integral(f: integrable_fun): { F: [T -> real] | 
                                       derivable?(F) AND deriv(F) = f }


   integral_lem: LEMMA integrable?(f) AND integral(f) = F AND 
                       derivable?(G) AND deriv(G) = f
                             IMPLIES (EXISTS (c: real): F = G + const_fun(c))


   deriv_integ: LEMMA derivable?(F) IMPLIES integrable?[T](deriv(F))



   indef_integral_thm : THEOREM derivable?(F) IMPLIES
                                (EXISTS (c: real): 
                                    integral(deriv(F)) = F + const_fun(c))


   fundamental_indef  : THEOREM continuous?(f) IMPLIES 
                                  Integrable?(a,b,f) AND
                                  Integral(a,b,f) = integral(f)(b) - integral(f)(a)




END indefinite_integral

quality93%

[ zur Elbe Produktseite wechseln0.14Quellennavigators  Analyse erneut starten  ]