Quelle sigma.pvs Sprache: PVS

sigma[T: TYPE FROM int]: THEORY
%------------------------------------------------------------------------------
% The summations theory introduces and defines properties of the sigma
% function that sums an arbitrary function F: [T -> real] over a range
% from low to high
%
%             high
%           ----
%  sigma(low, high, F) =  \     F(j)
%           /
%           ----
%          j = low
%
%  NOTE:
%
%     This is the generic theory.  It is usually preferable to use
%     sigma_nat, sigma_int, sigma_below, etc.
%
%  MODIFICATIONS:
%
%    8/7/01   added sigma_zero, sigma_with
%
%    3/24/06  generalized to allow index ranges to fall outside of
%             domain of T when high < low.  This upgrade will break
%             some old proofs, but will reduce TCC generation significantly
%
%    11/7/07  replace sigma with simpler definition.  Old definition available in
%             old_sigma_*.pvs theories.  Also old definition is retained as
%             sigma2.
%
%  AUTHORS:
%%    Rick Butler     NASA Langley Research Center
%    Paul Miner      NASA Langley Research Center
%
%------------------------------------------------------------------------------

BEGIN

  ASSUMING

     connected_domain: ASSUMPTION (FORALL (x, y: T), (z: integer):
                                       x <= z AND z <= y IMPLIES T_pred(z))

  ENDASSUMING

  T_low?: MACRO set[int] = {i:int | EXISTS (j:T): j <= i}
  T_low  : TYPE = {i:int | T_pred(i) OR T_low?(i)}

  T_high?: MACRO set[int] = {i:int | EXISTS (j:T): i <= j}
  T_high : TYPE = {i:int | T_pred(i) OR T_high?(i)}

  low,low1,low2       : VAR T_low
  high,high1,high2      : VAR T_high
  l,h,n,m,i : VAR T
  rng, nn   : VAR nat
  pn        : VAR posnat
  z,z1,z2         : VAR int
  a,x,B     : VAR real

  T_pred_lem : LEMMA low <= z AND z <= high IMPLIES T_pred(z)

% AUTO_REWRITE+ T_pred_lem  %% THIS DOES NOT HELP

% T_pred_low : LEMMA low <= m IMPLIES T_pred(low)
% T_pred_high: LEMMA m <= high IMPLIES T_pred(high)
%  AUTO_REWRITE+ T_pred_low, T_pred_high  %% DOES NOT HELP

  high_low_rewrite: LEMMA
   (FORALL (p: pred[[T_high, T_low]]):
     (FORALL (high: T_high), (low: T_low):
      IF high < low THEN p(high, low)
      ELSE (FORALL (n: subrange(low, high)): p(n, low))
      ENDIF)
    IMPLIES
      (FORALL high, low:  p(high, low)))

  F, G: VAR function[T -> real]

  % *** NEW *** Simpler Definition
  sigma(low, high, F): RECURSIVE real
      = IF low > high THEN 0
        ELSE  F(high) + sigma(low, high-1, F)
        ENDIF
   MEASURE (LAMBDA low, high, F: abs(high+1-low))

  % *** Old Definition ***
  sigma2(low, high, F): RECURSIVE real
      = IF low > high THEN 0
        ELSIF high = low THEN F(low)
        ELSE  F(high) + sigma2(low, high-1, F)
        ENDIF
   MEASURE (LAMBDA low, high, F: abs(high+1-low))

  % provides one unfolding analogous to old definition -- useful for upgrade
  sigma_rew : LEMMA sigma(low, high, F) = IF low > high THEN 0
                                          ELSIF high = low THEN F(low)
                                          ELSE  F(high) + sigma(low, high-1, F)
                                          ENDIF

  sigma_rew2: LEMMA sigma(low, high, F) = sigma2(low, high, F)

  sigma_spl     : THEOREM T_pred(low + nn + rng) IMPLIES
                           sigma(low, low+nn+rng, F) =
                              sigma(low,low+nn,F) + sigma(low+nn+1,low+nn+rng,F)

  sigma_split   : THEOREM low - 1 <= z AND z <= high IMPLIES
                            sigma(low, high, F) =
                                     sigma(low, z, F) + sigma(z+1, high, F)

% Both of the following are now covered by sigma_split

%   sigma_split_l: THEOREM %T_pred(low-1) AND
%                           low-1 <= m AND m < high IMPLIES
%                             sigma(low, high, F) =
%                                      sigma(low, m, F) + sigma(m+1, high, F)

%   sigma_split_h: THEOREM low <= m AND m <= high AND T_pred(m+1) IMPLIES
%                             sigma(low, high, F) =
%                                      sigma(low, m, F) + sigma(m+1, high, F)

  sigma_diff    : THEOREM low - 1 <= z AND z <= high IMPLIES
                    sigma(low, high, F) - sigma(low, z, F) = sigma(z+1, high, F)

  sigma_diff_neg: THEOREM low - 1 <= z AND z <= high IMPLIES
                  sigma(low, z, F) - sigma(low, high, F) = - sigma(z+1, high, F)

  sigma_eq_arg  : THEOREM sigma(m, m, F) = F(m)

  sigma_first   : THEOREM high >= low IMPLIES
                           sigma(low, high, F) = F(low) + sigma(low+1, high, F)

  sigma_last    : THEOREM high >= low IMPLIES
                          sigma(low, high, F) = sigma(low, high-1, F) + F(high)

  sigma_middle : THEOREM high >= i AND i >= low IMPLIES
                          sigma(low, high, F) = sigma(low, i-1, F) + F(i) +
                                                sigma(i+1, high, F)

  sigma_const   : THEOREM sigma(low, high, (LAMBDA i: x)) =
                           IF high >= low THEN (high-low+1) * x ELSE 0 ENDIF

  sigma_zero    : THEOREM sigma(low, high, (LAMBDA i: 0)) = 0

  sigma_scal    : THEOREM sigma(low, high, (LAMBDA i: a * F(i)))
                             = a * sigma(low, high, F)

  % Sometimes sigma_scal does not rewrite if the scalar is on the right, so the next lemma is needed

  sigma_scal_right    : THEOREM sigma(low, high, (LAMBDA i: F(i)*a))
                             = sigma(low, high, F)*a

  sigma_bound   : THEOREM low - 1 <= high AND
                         (FORALL i: i >= low AND i <= high IMPLIES F(i) <= B)
                            IMPLIES sigma(low, high, F) <= B*(high-low+1) %was abs(high-low+1)

  sigma_abs     : THEOREM abs(sigma(low, high, F)) <=
                              sigma(low, high, LAMBDA (n: T): abs(F(n)))

  sigma_ge_0    : THEOREM (FORALL (n: subrange(low,high)): F(n) >= 0)
                                IMPLIES sigma(low,high,F) >= 0

  sigma_gt_0    : THEOREM low <= high AND
                          (FORALL (n: subrange(low,high)): F(n) > 0)
                                IMPLIES sigma(low,high,F) > 0

  sigma_shift_T : THEOREM (FORALL (i:T): T_pred(i+z)) IMPLIES
            sigma(low+z,high+z,F) =
                                    sigma(low,high, (LAMBDA (i:T): F(i+z)))

  sigma_shift_T2 : THEOREM T_pred(low+z) AND T_pred(high+z) IMPLIES
            sigma(low+z,high+z,F) =
                 sigma(low,high, (LAMBDA (i:T): IF T_pred(i+z) THEN F(i+z)
                                                ELSE 0 ENDIF))

% ------------------ Summation Involving Two Functions ------------------

  sigma_sum     : THEOREM sigma(low, high, F) + sigma(low, high, G)
                             = sigma(low, high, (LAMBDA i: F(i) + G(i)))

  sigma_minus   : THEOREM sigma(low, high, F) - sigma(low, high, G)
                             = sigma(low, high, (LAMBDA i: F(i) - G(i)))

  sigma_abs_bnd  : THEOREM (FORALL (i: subrange(low,high)): abs(F(i)) <= G(i))
                       IMPLIES sigma(low, high, LAMBDA (n: T): abs(F(n))) <=
                                        sigma(low, high, G)

  restrict(F, low, high): function[T -> real] =
     (LAMBDA i: IF i < low OR i > high THEN 0 ELSE F(i) ENDIF )

  sigma_restrict   : THEOREM l <= low AND h >= high IMPLIES
                            sigma(low,high,F) = sigma(low,high,restrict(F,l,h))

  sigma_restrict_to: THEOREM sigma(low,high,F) =
                                sigma(low,high,restrict(F,low,high))

  sigma_restrict_eq: THEOREM restrict(F,low,high) = restrict(G,low,high)
                                IMPLIES sigma(low,high,F) = sigma(low,high,G)

  sigma_shift_fun_eq: THEOREM high1-low1 = high2-low2 AND
                 (FORALL (i:subrange(0,high1-low1)): F(low1+i) = G(low2+i))
         IMPLIES
         sigma(low1,high1,F) = sigma(low2,high2,G)

  sigma_const_restrict_eq: LEMMA restrict(F,low,high) = restrict(G,low,high)
                                IMPLIES x*sigma(low,high,F) = x*sigma(low,high,G)

  sigma_restrict_eq_0: THEOREM (FORALL (i: subrange(low,high)): F(i) = 0)
                   IMPLIES sigma(low,high,F) = 0

  sigma_triangle: LEMMA abs(sigma(low,high,F))<=sigma(low,high,LAMBDA (n:T):abs(F(n)))

  sigma_eq_one_arg : THEOREM low<=z AND z<=high AND
               (FORALL (i:subrange(low,z-1)):F(i)=0) AND
        (FORALL (i:subrange(z+1,high)):F(i)=0) IMPLIES
        sigma(low,high,F) = F(z)

  sigma_eq_one_arg2 : THEOREM low<=z AND z<=high AND
               (FORALL (i:subrange(low,high)):i/=z IMPLIES F(i)=0) IMPLIES
        sigma(low,high,F) = F(z)

  sigma_eq_two_args: THEOREM low<=z1 AND z1<=high AND
               low<=z2 AND z2<=high AND z1/=z2 AND
        (FORALL (i:subrange(low,high)): i/=z1 AND i/=z2 IMPLIES F(i)=0)
        IMPLIES sigma(low,high,F) = F(z1)+F(z2)

  sigma_const_restrict_eq_0: THEOREM (FORALL (i: subrange(low,high)): F(i) = 0)
                   IMPLIES x*sigma(low,high,F) = 0

  sigma_eq         : THEOREM (FORALL (n: subrange(low,high)): F(n) = G(n))
                                IMPLIES sigma(low,high,F) = sigma(low,high,G)

  sigma_le         : THEOREM (FORALL (n: subrange(low,high)): F(n) <= G(n))
                                IMPLIES sigma(low,high,F) <= sigma(low,high,G)

  sigma_lt         : THEOREM low <= high AND
                             (FORALL (n: subrange(low,high)): F(n) < G(n))
                                IMPLIES sigma(low,high,F) < sigma(low,high,G)

  sigma_ge         : THEOREM (FORALL (n: subrange(low,high)): F(n) >= G(n))
                                IMPLIES sigma(low,high,F) >= sigma(low,high,G)

  sigma_gt         : THEOREM low <= high AND
                             (FORALL (n: subrange(low,high)): F(n) > G(n))
                                IMPLIES sigma(low,high,F) > sigma(low,high,G)

  sigma_with       : THEOREM low <= i AND i <= high AND
                             F = G WITH [i := a] IMPLIES
                          sigma(low, high,F) = sigma(low,high,G) - G(i) + a

  sigma_le_scal    : THEOREM low<=high AND
                      (FORALL (i): low<=i AND i<=high IMPLIES F(i)<=B/(high-low+1))
                      IMPLIES
        sigma(low,high,F)<=B



% ------------------------ Special Arguments --------------------------------

  sigma_nonneg     : THEOREM (FORALL i: F(i) >= 0)
                                 IMPLIES sigma(low, high, F) >= 0

  sigma_nonpos     : THEOREM (FORALL i: F(i) <= 0)
                                 IMPLIES sigma(low, high, F) <= 0

  Fnnr: VAR function[T -> nonneg_real]
  Fnpr: VAR function[T -> nonpos_real]
  Fnat: VAR function[T -> nat]
  Fnpi: VAR function[T -> nonpos_int]
  Fposnat: VAR function[T -> posnat]
  Fposreal: VAR function[T -> posreal]

  sigma_Fnnr        : LEMMA FORALL (Fnnr, high, low): sigma(low, high, Fnnr) >= 0

  sigma_nnreal      : JUDGEMENT sigma(low,high,Fnnr) HAS_TYPE nnreal

  sigma_nonpos_real : JUDGEMENT sigma(low,high,Fnpr) HAS_TYPE nonpos_real

  sigma_nat         : JUDGEMENT sigma(low,high,Fnat) HAS_TYPE nat

  sigma_nonpos_int  : JUDGEMENT sigma(low,high,Fnpi) HAS_TYPE nonpos_int

  sigma_posnat      : LEMMA low <= high IMPLIES sigma(low,high,Fposnat) > 0

  sigma_posreal     : LEMMA low <= high IMPLIES sigma(low,high,Fposreal) > 0

  sigma_nonneg_eq_0 : THEOREM sigma(low,high,Fnnr) = 0
                              AND low <= i AND i <= high IMPLIES Fnnr(i) = 0

  sigma_nn_ge_comps : THEOREM low <= i AND i <= high IMPLIES
                                  sigma(low,high,Fnnr) >= Fnnr(i)

% ------------------- Iterative Summation (tail recursion) ------------

   sum_it_def(low, high, F,a): RECURSIVE real
      = IF low > high THEN a
        ELSE  sum_it_def(low+1,high,F,a+F(low))
        ENDIF
   MEASURE (LAMBDA low, high, F, a: abs(high+1-low))

   sum_it(low,high,F) : real = sum_it_def(low,high,F,0)

   sum_it_prop : LEMMA
     low - 1 <= i AND i <= high =>
     sum_it_def(i+1,high,F,sigma(low,i,F)) = sigma(low,high,F)

   sum_it_sigma: LEMMA sum_it(low,high,F) = sigma(low,high,F)

   sigma_it(low,high,F) : MACRO real = sum_it(low,high,F)

% Note: We would have preferred to use the following definitions:
%
%   T_low?: MACRO set[int] = {i:int | EXISTS (j:T): j <= i}
%   T_low  : TYPE = {i:int | T_low?(i)}
%
%   T_high?: MACRO set[int] = {i:int | EXISTS (j:T): i <= j}
%   T_high : TYPE = {i:int | T_high?(i)}
%
% but could not find any judgements that would fire and prevent
% spurious TCC generation.

END sigma

quality94%

¤ Dauer der Verarbeitung: 0.17 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.