Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/trig_fnd/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 10 kB

Quelle trig_approx.pvs Sprache: PVS

trig_approx: THEORY
%-----------------------------------------------------------------------------
%      trig_approx
%      -----------
%          - taylor series approximations to trig functions:
%               sin_approx(a,n): sum first n terms of taylor expansion of sin
%               cos_approx(a,n): sum first n terms of taylor expansion of cos
%          - defines upper and lower bounds on trig functions:
%
%       Version 2 Foundational (DRL) 4/4/05
%
%  CHANGES
%    - Redefined sin_lb,sin_ub,cos_lb,cos_ub,tan_lb,tan_ub to make it
%      suitable for interval theory.
%    - Removed lemmas SIN,COS,TAN. Use sin_bound_0_pi, cos_bound_npi2_pi2,
%      tan_bound_0_pi2. Cesar Munoz (Nov 28 2003).
%    - Added Hanne Gottliebsen's proofs for sin_bound_npi_0 and
%      cos_bound_npi_pi.
%      Cesar Munoz (Feb 6 2004).
%    - Tan approximations moved to tan_approx due to circularity problems with
%      trig_ineq. Cear Munoz (Feb 6 2004)
%    - The theory has been completely revisited by David Lester (4/4/05)
%
%-----------------------------------------------------------------------------

  BEGIN

  IMPORTING  exp_term, sincos, trig_ineq, reals@sigma_nat,
             analysis@derivatives,trig_extra,analysis@derivative_props

  m,n:  VAR nat
  pm:   VAR posnat
  a:    VAR real
  px:   VAR posreal
  n0x:  VAR nzreal
  nnx:  VAR nnreal

  IMPORTING analysis@deriv_domains

  sin_term(a)(n): real = (-1)^n*a^(2*n+1)/factorial(2*n+1)

  sin_term_next       : LEMMA sin_term(a)(n+1) =
                              sin_term(a)(n) * -1 * a*a / ((2*n+3)*(2*n+2))

  sin_term_neg        : LEMMA sin_term(-a)(n) = -sin_term(a)(n)

  sin_terms_alternate : LEMMA 0 /= a IMPLIES (sin_term(a)(n+1) < 0 IFF
                                                sin_term(a)(n) > 0)

  sin_term_nonzero    : LEMMA sin_term(a)(n) /= 0 IFF a /= 0
  sin_term_zero       : LEMMA sin_term(a)(n)  = 0 IFF a  = 0
  sin_term_gt0        : LEMMA sin_term(a)(n)  > 0 IFF
                           ((even?(n) AND a > 0) OR (odd?(n) AND a < 0))
  sin_term_lt0        : LEMMA sin_term(a)(n)  < 0 IFF
                           ((even?(n) AND a < 0) OR (odd?(n) AND a > 0))

  sin_tends_to_0      : LEMMA tends_to_0?(sin_term(a))

  cos_term(a)(n): real = IF n=0 THEN 1 ELSE (-1)^n*a^(2*n)/factorial(2*n) ENDIF

  cos_term_next       : LEMMA cos_term(a)(n+1) =
                              cos_term(a)(n) * -1 * a*a / ((2*n+2)*(2*n+1))

  cos_term_neg        : LEMMA cos_term(-a)(n) = cos_term(a)(n)

  cos_terms_alternate : LEMMA 0 /= a IMPLIES (cos_term(a)(n+1) < 0 IFF
                                                cos_term(a)(n) > 0)

  cos_term_nonzero    : LEMMA cos_term(a)(n) /= 0 IFF (n  = 0   OR  a /= 0)
  cos_term_zero       : LEMMA cos_term(a)(n)  = 0 IFF (n /= 0   AND a  = 0)
  cos_term_gt0        : LEMMA cos_term(a)(n)  > 0 IFF
                                   (even?(n) AND (a /= 0 OR n = 0))
  cos_term_lt0        : LEMMA cos_term(a)(n)  < 0 IFF (odd?(n) AND a /= 0)

  cos_tends_to_0      : LEMMA tends_to_0?(cos_term(n0x))

  sin_term_deriv: LEMMA derivable?[real](LAMBDA a: sin_term(a)(n)) AND
      deriv[real](LAMBDA a: sin_term(a)(n)) = (LAMBDA a: cos_term(a)(n))

  cos_term_deriv: LEMMA derivable?[real](LAMBDA a: cos_term(a)(n)) AND
      deriv[real](LAMBDA a: cos_term(a)(n)) =
                      (LAMBDA a: IF n = 0 THEN 0 ELSE -sin_term(a)(n-1) ENDIF)

  sin_approx(a,n):real = sigma(0,n,sin_term(a))

  sin_approx_a0:     LEMMA sin_approx(0,n) = 0

  sin_approx_neg:    LEMMA sin_approx(-a,n) = -sin_approx(a,n)

  sin_approx_next:   LEMMA sin_approx(a,n+2) - sin_approx(a,n) =
                            sin_term(a)(n+1) * (1 - a*a/((2*n+5)*(2*n+4)))

  sin_approx_eq:     LEMMA a*a = (2*n+5)*(2*n+4) IMPLIES
                            sin_approx(a,n+2) = sin_approx(a,n)

  sin_approx_sin:    LEMMA abs(sin(a)-sin_approx(a,n)) <= abs(sin_term(a)(n+1))

  cos_approx(a,n):real = sigma(0,n,cos_term(a))

  cos_approx_a0:     LEMMA cos_approx(0,n) = 1

  cos_approx_neg:    LEMMA cos_approx(-a,n) = cos_approx(a,n)

  cos_approx_cos:    LEMMA abs(cos(a)-cos_approx(a,n)) <= abs(cos_term(a)(n+1))

  cos_approx_next:   LEMMA cos_approx(a,n+2) - cos_approx(a,n) =
                            cos_term(a)(n+1) * (1 - a*a/((2*n+4)*(2*n+3)))

  cos_approx_eq:     LEMMA a*a = (2*n+4)*(2*n+3) IMPLIES
                            cos_approx(a,n+2) = cos_approx(a,n)

  sin_approx_deriv: LEMMA derivable?[real](LAMBDA a: sin_approx(a,n)) AND
                    deriv[real](LAMBDA a: sin_approx(a,n))
                                                 = (LAMBDA a: cos_approx(a,n))

  cos_approx_deriv: LEMMA derivable?[real](LAMBDA a: cos_approx(a,n)) AND
                    deriv[real](LAMBDA a: cos_approx(a,n)) =
                      (LAMBDA a: IF n = 0 THEN 0 ELSE -sin_approx(a,n-1) ENDIF)

  sin_ub(a,n):real = IF a < 0 THEN sin_approx(a,2*n+1)
                              ELSE sin_approx(a,2*n)   ENDIF
  sin_lb(a,n):real = IF a < 0 THEN sin_approx(a,2*n)
                              ELSE sin_approx(a,2*n+1) ENDIF

  sin_lb_neg: LEMMA sin_lb(-a,n) = -sin_ub(a,n)
  sin_ub_neg: LEMMA sin_ub(-a,n) = -sin_lb(a,n)

  sin_lb_a0 : LEMMA sin_lb(0,n) = 0
  sin_ub_a0 : LEMMA sin_ub(0,n) = 0

  sin_lb_ub : LEMMA sin_lb(n0x,n) < sin_ub(n0x,n)

  sin_lb_inc: LEMMA px*px < (4*n+7)*(4*n+6) => sin_lb(px,n) < sin_lb(px,n+pm)
  sin_ub_dec: LEMMA px*px < (4*n+5)*(4*n+4) => sin_ub(px,n+pm) < sin_ub(px,n)

  sin_lb_lt : LEMMA px*px < (4*n+7)*(4*n+6) => sin_lb(px,n) < sin(px)
  sin_ub_lt : LEMMA px*px < (4*n+5)*(4*n+4) => sin(px) < sin_ub(px,n)

  sin_lb_gt : LEMMA px*px > (4*n+7)*(4*n+6) => sin_lb(px,n) < -1
  sin_ub_gt : LEMMA px*px > (4*n+5)*(4*n+4) => sin_ub(px,n) >  1

  sin_lb     : LEMMA sin_lb(n0x,n) < sin(n0x)
  sin_ub     : LEMMA sin(n0x) < sin_ub(n0x,n)
  sin_bounds : LEMMA sin_lb(a,n) <= sin(a) AND sin(a) <= sin_ub(a,n)

  sin_lb_gt0: LEMMA px*px < 6 => sin_lb(px,n) > 0

  cos_ub(a,n):real = cos_approx(a,2*n)
  cos_lb(a,n):real = cos_approx(a,2*n+1)

  cos_lb_neg: LEMMA cos_lb(-a,n) = cos_lb(a,n)
  cos_ub_neg: LEMMA cos_ub(-a,n) = cos_ub(a,n)

  cos_lb_a0 : LEMMA cos_lb(0,n) = 1
  cos_ub_a0 : LEMMA cos_ub(0,n) = 1

  cos_lb_ub: LEMMA cos_lb(n0x,n) < cos_ub(n0x,n)

  cos_lb_inc: LEMMA n0x*n0x<(4*n+6)*(4*n+5) => cos_lb(n0x,n) < cos_lb(n0x,n+pm)
  cos_ub_dec: LEMMA n0x*n0x<(4*n+4)*(4*n+3) => cos_ub(n0x,n+pm) < cos_ub(n0x,n)

  cos_lb_lt:  LEMMA n0x*n0x < (4*n+6)*(4*n+5) => cos_lb(n0x,n) < cos(n0x)
  cos_ub_lt:  LEMMA n0x*n0x < (4*n+4)*(4*n+3) => cos(n0x) < cos_ub(n0x,n)

  cos_lb_gt:  LEMMA n0x*n0x > (4*n+6)*(4*n+5)        => cos_lb(n0x,n) < -1
  cos_ub_gt:  LEMMA n0x*n0x > (4*n+4)*(4*n+3) & n>=1 => cos_ub(n0x,n) >  1

  cos_lb:     LEMMA cos_lb(n0x,n) < cos(n0x)
  cos_ub:     LEMMA cos(n0x) < cos_ub(n0x,pm)

  cos_bounds:  LEMMA cos_lb(a,n) <= cos(a) AND cos(a) <= cos_ub(a,n)

  sin_lb_deriv: LEMMA derivable?[nnreal](LAMBDA nnx: sin_lb(nnx,n)) AND
       deriv[nnreal](LAMBDA nnx: sin_lb(nnx,n)) = (LAMBDA nnx: cos_lb(nnx,n))

  sin_ub_deriv: LEMMA derivable?[nnreal](LAMBDA nnx: sin_ub(nnx,n)) AND
       deriv[nnreal](LAMBDA nnx: sin_ub(nnx,n)) = (LAMBDA nnx: cos_ub(nnx,n))

  cos_lb_deriv: LEMMA derivable?[real](LAMBDA a: cos_lb(a,n)) AND
       deriv[real](LAMBDA a: cos_lb(a,n))
         = (LAMBDA a: IF a < 0 THEN -sin_lb(a,n) ELSE -sin_ub(a,n) ENDIF)

  cos_ub_deriv: LEMMA derivable?[real](LAMBDA a: cos_ub(a,n)) AND
       deriv[real](LAMBDA a: cos_ub(a,n))
         = (LAMBDA a: IF n = 0 THEN 0 ELSIF
                         a < 0 THEN -sin_ub(a,n-1) ELSE -sin_lb(a,n-1) ENDIF)

  cos_lb_nn_strict_decreasing:
        LEMMA strict_decreasing?(LAMBDA (x:{x:nnreal| x <=  pi}): cos_lb(x,n))

  cos_lb_np_strict_increasing:
        LEMMA strict_increasing?(LAMBDA (x:{x:npreal| x >= -pi}): cos_lb(x,n))

  sin_px: LEMMA 1/500 > px => sin(px) > px*(1-1/1500000)

  % Approximation to guarantee cos_lb > 0
  Cos_pos_n : MACRO posnat = 5

  cos_term_pi_lb: LEMMA n >= Cos_pos_n IMPLIES
                        cos_term(pi_lbn(n)/2)(2*n+2) < cos(pi_lbn(n)/2)

  cos_lb_pi2_eps: LEMMA px <= pi/2 AND
                        abs(cos_term(pi/2-px)(2*n+2)) < sin(px) =>
                        cos_lb(pi/2-px,n) > 0

  cos_lb_pi2_pos0 : LEMMA n=0 => NOT cos_lb(pi_lbn(n)/2,n) > 0

  cos_lb_pi2_pos1 : LEMMA n=1 => NOT cos_lb(pi_lbn(n)/2,n) > 0

  cos_lb_pi2_pos2 : LEMMA n=2 => NOT cos_lb(pi_lbn(n)/2,n) > 0

  cos_lb_pi2_pos : LEMMA
    n >= Cos_pos_n IMPLIES
    cos_lb(pi_lbn(n)/2,n) > 0

  % Approximation to guarantee sin_lb > 0
  Sin_pos_n : MACRO posnat = 11

  sin_term_pi_lb: LEMMA n >= Sin_pos_n IMPLIES
                        sin_term(pi_lbn(n+1))(2*n+2) < sin(pi_lbn(n+1))

  sin_lb_pi_not_pos: LEMMA
    FORALL (b9:below(11)):
    NOT sin_lb(pi_lbn(b9+1),b9) > 0

  sin_lb_pi_pos: LEMMA
    n >= Sin_pos_n IMPLIES
    sin_lb(pi_lbn(n+1),n) > 0

  pi_lb_est(n:nat): {rr:nnreal | rr < pi} =
    IF n < 12 THEN pi_lbn(n)-2/(n^3+1)
    ELSE pi_lbn(n) ENDIF

  pi_lb_est_le: LEMMA pi_lb_est(n) <= pi_lbn(n) AND pi_lb_est(n) <= pi

  sin_lb_pi_est_pos: LEMMA sin_lb(pi_lb_est(n+1),n) > 0

  sin_lb_pi_range_pos: LEMMA
    px <= pi_lb_est(n+1) IMPLIES sin_lb(px,n) > 0

  % Monotonicity of cos_ub

  cos_ub_nn_strict_decreasing:
        LEMMA n>=1 IMPLIES
strict_decreasing?(LAMBDA (x:{x:nnreal| x <=  pi_lb_est(n)}): cos_ub(x,n))

  cos_ub_np_strict_increasing:
        LEMMA n>=1 IMPLIES
strict_increasing?(LAMBDA (x:{x:npreal| x >= -pi_lb_est(n)}): cos_ub(x,n))

  % Monotonicity of sin_lb and sin_ub

  sin_lb_increasing: LEMMA
    strict_increasing?(LAMBDA (x:{x:real| -pi_lb_est(n)/2 <= x AND x <= pi_lb_est(n)/2}): sin_lb(x,n))

  sin_ub_increasing: LEMMA
    strict_increasing?(LAMBDA (x:{x:real| -pi_lb_est(n)/2 <= x AND x <= pi_lb_est(n)/2}): sin_ub(x,n))

  sin_lb_nn_decreasing: LEMMA
    strict_decreasing?(LAMBDA (x:{x:real | pi/2 <= x AND x <= pi}): sin_lb(x,n))

  cos_term_pi_ub: LEMMA n >= Cos_pos_n IMPLIES
                        -cos_term(pi_ubn(n)/2)(2*n+1) < -cos(pi_ubn(n)/2)

  cos_ub_pi2_neg : LEMMA
    n >= Cos_pos_n IMPLIES
    cos_ub(pi_ubn(n)/2,n) < 0

  pi_ub_est(n:nat): {rr:nnreal | pi < rr AND rr < 3*pi/2} =
    IF n < 5 THEN pi_ubn(n)+1/(n+1)^4
    ELSE pi_ubn(n) ENDIF

  sin_ub_nn_decreasing: LEMMA n>=1 IMPLIES
    strict_decreasing?(LAMBDA (x:{x:real | pi_ub_est(n)/2 <= x AND x <= pi_lb_est(n)}): sin_ub(x,n))

END trig_approx

quality80%

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