Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: indefinite_integral.pvs   Sprache: Unknown

indefinite_integral[T: TYPEFROM 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



[ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik