Quelle  asin.pvs

asin: THEORY

  BEGIN
 
  IMPORTING reals@sq, reals@sqrt
  IMPORTING atan
%  IMPORTING analysis@sqrt_derivative, analysis@derivative_props

%  real_abs_le1:    NONEMPTY_TYPE = {x:real | abs(x) <= 1}    CONTAINING 0
%  real_abs_lt1:    NONEMPTY_TYPE = {x:real | abs(x) <  1}    CONTAINING 0
%  real_abs_le_pi2: NONEMPTY_TYPE = {x:real | abs(x) <= pi/2} CONTAINING 0
  real_abs_le1:   NONEMPTY_TYPE =  {x:real | -1 <= x AND x <= 1}    CONTAINING 0
  real_abs_lt1:   NONEMPTY_TYPE =  {x:real | -1 < x  AND x <  1}    CONTAINING 0
  real_abs_le_pi2: NONEMPTY_TYPE = {x:real | -pi/2 <= x AND x <= pi/2} CONTAINING 0

  x,y:     VAR real_abs_le1
  xne:     VAR real_abs_lt1
  nnx,nny: VAR {x:nnreal | x <= 1}
  nx:      VAR {x:real_abs_le1 | x < 0}
  px:      VAR {x:real_abs_le1 | 0 < x}
  nx_gt1:  VAR {x:negreal | -1 < x}
  px_lt1:  VAR {x:posreal | x < 1}

  asin(x:real_abs_le1):real_abs_le_pi2
    = IF x = -1 THEN -pi/2 ELSIF x < 1 THEN atan(x/sqrt(1-x*x)) ELSE pi/2 ENDIF

  asin_neg_restrict:      LEMMA asin(nx) = -pi/2 - atan(sqrt(1-nx*nx)/nx)
  asin_pos_restrict:      LEMMA asin(px) =  pi/2 - atan(sqrt(1-px*px)/px)
  asin_0:                 LEMMA asin(0)  = 0
  asin_sqrt_half:         LEMMA asin(sqrt(1/2)) = pi/4
  asin_1:                 LEMMA asin(1)  = pi/2
  asin_neg:               LEMMA asin(-x) = -asin(x)
  asin_minus1:            LEMMA asin(-1) = -pi/2
  asin_minus_sqrt_half:   LEMMA asin(-sqrt(1/2)) = -pi/4
  asin_strict_increasing: LEMMA strict_increasing?(asin)
  asin_bij:               LEMMA bijective?[real_abs_le1,real_abs_le_pi2](asin)

  asin_diff: LEMMA                                                     % 4.4.32
      asin(nnx)-asin(nny) = asin(nnx*(sqrt(1-sq(nny)))-nny*(sqrt(1-sq(nnx))))

%   asin_derivable:  LEMMA
%                 derivable[real_abs_lt1]((LAMBDA (x:real_abs_lt1):asin(x)),xne)
%   asin_derivable2: LEMMA
%                 derivable[real_abs_lt1](LAMBDA (x:real_abs_lt1): asin(x))
%   deriv_asin_fun:  LEMMA deriv[real_abs_lt1](LAMBDA (x:real_abs_lt1): asin(x))
%                            = (LAMBDA (x:real_abs_lt1): 1/sqrt(1-sq(x)))

  asin_pos_bnds: AXIOM px < asin(px) AND
             (px*(1-px*px/6) > 0 => asin(px*(1-px*px/6)) < px)

  END asin