Quelle integral_pulse.pvs Sprache: 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

quality93%

¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.