| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle cont_if_fun.pvs Sprache: PVS |
|||||||||
|
cont_if_fun[ T : TYPE FROM real] : THEORY
%------------------------------------------------------------------------------- % % Continuity of a function defined using an IF-THEN-ELSE % % G = IF <expr> THEN f1 ELSE f2 ENDIF % % is continuous if f1 and f2 are continuous and they are equal at all of the % place where the <expr> is discontinuous. % % Author: Rick Butler NASA Langley % Jan 22, 2009 %------------------------------------------------------------------------------- BEGIN ASSUMING connected_domain : ASSUMPTION FORALL (x, y : T), (z : real) : x <= z AND z <= y IMPLIES T_pred(z) ENDASSUMING IMPORTING continuous_functions[T] f,f1,f2 : VAR [T -> real] P : VAR [T -> bool] a, b, c, d, x : VAR T discont_pts(P): set[T] = {x:T | NOT continuous_at?(P,x)} discont_pts_lem: LEMMA NOT discont_pts(P)(a) IMPLIES EXISTS (delta: posreal): (FORALL (x:T): abs(x-a) < delta IMPLIES P(x) = true) OR (FORALL (x:T): abs(x-a) < delta IMPLIES P(x) = false) if_fun(P: [T-> bool], f1:[T -> real], f2:[T -> real]): [T -> real] = (LAMBDA (x:T): IF P(x) THEN f1(x) ELSE f2(x) ENDIF) if_fun_cont: LEMMA continuous?(f1) AND continuous?(f2) AND (FORALL (x:T): discont_pts(P)(x) IMPLIES f1(x) = f2(x)) IMPLIES continuous?(if_fun(P,f1,f2)) discont_pts_simple: LEMMA continuous?(f1) AND continuous?(f2) AND P = (LAMBDA (t: T): f1(t) > 0 AND f2(t) > 0) AND discont_pts(P)(x) IMPLIES f1(x) = 0 OR f2(x) = 0 prod_fun_lem: LEMMA continuous?(f1) AND continuous?(f2) AND P = (LAMBDA (t: T): f1(t) > 0 AND f2(t) > 0) AND discont_pts(P)(x) IMPLIES f1(x)*f2(x) = -abs(f1(x)*f2(x)) END cont_if_fun ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28