| products/Sources/formale Sprachen/Delphi/Autor 0.7/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sigma.pvs Sprache: PVSOriginal von: 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 ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
