Go backward to 4.3 The Specification DefineBasicReal
Go up to 4 A Specification of Real Numbers
Go forward to 4.5 The Specification CompactBasicReal

## 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

CoFI Note: M-7 -- Version: 0.2 -- 13 April 1999.