Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: integral_pulse.pvs Sprache: PVS

Original von: PVS^©

integral_pulse[T: TYPE FROM real]: THEORY
%----------------------------------------------------------------------------
%
%  Integral of:
%
%                    |-------------------|    c
%                    |                   |
%                    |                   |
%     ---------------|                   |-----------------
%                   xl                   xh
%
%
%  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 integral_prep[T], reals@sigma_upto

   a,b,x,y,z: VAR T
   c:         VAR real
   f,g:       VAR [T -> real]
   xl,xh:     VAR T

   EX3p: LEMMA  a < b IMPLIES (FORALL (P: partition(a,b),p,q:nat):
                  0 < p AND p <= q AND q <= length(P) - 1 IMPLIES
                  sigma(p, q, (LAMBDA (n: upto(length(P) - 1)):
                  IF n = 0 THEN 0 ELSE seq(P)(n) - seq(P)(n - 1) ENDIF)) =
                         seq(P)(q) - seq(P)(p-1))

   ii: VAR nat
   EE: VAR posreal
   EXse: LEMMA a < b IMPLIES FORALL (P: partition(a,b),
                                     xis: (xis?(a,b,P))):
               0 < ii AND ii < length(P)
               AND (FORALL z:
                   (IF xl < z AND z < xh THEN f(z) = 1 ELSE f(z) = 0 ENDIF))
               AND width(a, b, P) < EE
               IMPLIES abs(Rie_sec(a, b, P, xis, f, ii)) < EE

%  Rosenlicht page 114

   Example_3: LEMMA a <= xl AND xl < xh AND xh <= b AND
                  (FORALL z: (IF xl < z AND z < xh THEN f(z) = 1
                                ELSE f(z) = 0 ENDIF))
                           IMPLIES integrable?(a,b,f) AND
                                   integral(a,b,f) = xh-xl

%
%  only one point where function is nonzero: Rosenlicht Ex 2 pg 114
%

   zero_except?(a,b,f): bool = a < b AND
                          (EXISTS z,c: a <= z AND z <= b AND f(z) = c AND
                                 (FORALL x: x /= z IMPLIES f(x) = 0))

   zero_except?_integrable: LEMMA a < b AND zero_except?(a,b,f) IMPLIES
                               integrable?(a,b,f) AND integral(a,b,f) = 0

   zero_not_intv?(xl,xh,f,c): bool =
                         (FORALL z:
                             IF xl < z AND z < xh THEN f(z) = c
                             ELSE  f(z) = 0
                             ENDIF)

   zero_not_intv?_integrable: LEMMA a <= xl AND xl < xh AND xh <= b AND
               zero_not_intv?(xl,xh,f,c) IMPLIES integrable?(a,b,f)
               AND integral(a,b,f) = c*(xh-xl)

%  ---------- doesn't matter what the value is at xl and xh -------------

   zero_except_intv?(xl,xh,c,f): bool =
                         (FORALL z:
                             (xl < z AND z < xh IMPLIES f(z) = c) AND
                             (z < xl IMPLIES f(z) = 0) AND
                             (z > xh IMPLIES f(z) = 0)  )

%  generalization of Example 3

   zero_except_intv?_integrable: LEMMA a <= xl AND xl < xh AND xh <= b AND
               zero_except_intv?(xl,xh,c,f) IMPLIES
                     integrable?(a,b,f) AND
                     integral(a,b,f) = c*(xh-xl)

END integral_pulse

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.