Quelle  asinx.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Arcsine
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

asinx: THEORY

BEGIN

  IMPORTING atanx, trig_fnd@asin

  cauchy_real_abs_le1?(c:[nat->int]):bool
                         = EXISTS (x:real_abs_le1): cauchy_prop(x,c)

  cauchy_real_abs_le1: NONEMPTY_TYPE
                         = (cauchy_real_abs_le1?) CONTAINING (LAMBDA (p:nat):0)

  JUDGEMENT cauchy_real_abs_le1 SUBTYPE_OF cauchy_real

  x:  VAR real_abs_le1
  cx: VAR cauchy_real_abs_le1

%  asin x  = if x0 >  0 then piBy2 - atan (s/x) else
%            if x0 == 0 then atan (x/s)         else
%            {- x0 <  0 -}   atan (s/x) - piBy2
%            where (CR_ x') = x; x0 = x' 0; s = sqrt (fromInteger 1 - x*x)

  cauchy_asin(cx):cauchy_real
    = LET t  = cx(0),
          s  = cauchy_sqrt(cauchy_sub(cauchy_int(1),cauchy_mul(cx,cx))),
          p2 = cauchy_div2n(cauchy_pi,1)
      IN IF    t = 0 THEN cauchy_atan(cauchy_div(cx,s))
         ELSE LET a  = cauchy_atan(cauchy_div(s,cx)) IN
         IF t > 0 THEN cauchy_sub(p2,a)
                  ELSE cauchy_sub(cauchy_neg(p2),a) ENDIF ENDIF

  asin_lemma: LEMMA cauchy_prop(x,cx) IMPLIES
                                          cauchy_prop(asin(x),cauchy_asin(cx))

END asinx