4.4 The Specification BasicReal

In this draft version the definedness predicates for the standard functions in the following specification do not respect our rule of methodology from Note M-6 [RM99a]. A general problem is that the domain of convergence of the taylor series is not obvious. Therefore we prefer at the moment to specify the domains of the functions explicitly.

spec

 BasicReal[DefineBasicReal] =

%def

ops

exp :	Real -> Real;
ln,sqrt :	Real ->? Real;
e :	Real;
__ ^ __ :	Real × Real ->? Real;
sin, cos, sinh, cosh :	Real -> Real;
tan, cot, arcsin, arccos,
arctan, arccot, tanh, coth,
arsinh, arcosh, artanh, arcoth :	Real ->? Real;
pi :	Real;

vars

x,y:Real

%%

we use Taylor series for exp, ln, sin, cos, arcsin -

%%

the other functions can be defined in terms of these:

%%

exp(x), e:

.

exp(x) = sum( constSeq(x) ^ N / (N !) )

.

e = exp(1)

%%

ln(x):

.

defln(x) <=> x > 0

.

ln(x) = sum(	constSeq(x-1) ^ (2*N+1) /
	( (2*N+1) * (constSeq(x+1) ^ (2*N+1)) ))
	if defln(x)

%%

x ^ y:

.

defx ^ y <=> x > 0

.

x ^ y = exp(ln(x)*y)

%%

sqrt(x):

.

defsqrt(x) <=> x > 0

.

sqrt(0) = 0

.

sqrt(x) = x ^ (1/2) if x>0

%%

sin(x) and cos(x):

.

sin(x) = sum( (-1) ^ N * constSeq(x) ^ (2*N+1) / (2*N+1)! )

.

cos(x) = sum( (-1) ^ N * constSeq(x) ^ (2*N) / (2*N)! )

%%

tan(x) and cot(x):

.

deftan(x) <=> ¬ exists z: Int . x= (2*z+1) * pi/2

.

tan(x) = sin(x) / cos(x) ifdeftan(x)

.

defcot(x) <=> ¬ exists z: Int . x= 2* z * pi/2

.

cot(x) = cos(x) / sin(x) ifdefcot(x)

%%

arcsin(x) and pi:

.

defarcsin(x) <=> abs(x) < 1

.

arcsin(x) = sum(	(2*N+1)!* constSeq(x) ^ (2*N+1) /
	( (2*N+1)*2 ^ (2*N-1)*(N-1)!*N! ))
if defarcsin(x)

.

pi = 4*arcsin(sqrt(1/2))

.

arcsin(1) = pi/2

.

arcsin(-1) = -pi/2

%%

arccos(x):

.

defarccos(x) <=> abs(x) < 1

.

arccos(x) = pi/2-arcsin(x) if defarccos(x)

%%

cyclometric functions:

.

arctan(x) = arcsin(x/sqrt(1+x ^ 2))

.

arccot(x) = arccos(x/sqrt(1+x ^ 2))

%%

hyperbolic functions:

.

sinh(x) = (exp(x)-exp(-x))/2

.

cosh(x) = (exp(x)+exp(-x))/2

.

tanh(x) = sinh(x)/cosh(x)

.

coth(x) = cosh(x)/sinh(x)

%%

area functions:

.

arsinh(x) = ln(x+sqrt(x ^ 2+1))

.

arcosh(x) = arsinh(sqrt(x ^ 2+1))

.

artanh(x) = arsinh(x/sqrt(1-x ^ 2))

.

arcoth(x) = arsinh(1/sqrt(x ^ 2-1))

end

view

 CommutativeField_in_BasicReal:

DefineCommutativeField to BasicReal =

sorts

Elem |-> Real,

ops

0 |-> 0,

1 |-> 1,

__+__ |-> __+__,

__*__ |-> __*__

end

view

 TotalOrder_in_BasicReal:

TotalOrder

to BasicReal =

sort

Elem ^_|-> Real,

pred

__ < __ ^_|-> __ < __

end