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