Basic Reals
spec
DefineOrderedField =
DefineCommutativeField and TotalOrder
then
vars
a,b,c:Elem
. a+c <= b+c if a <= b
. a*c <= b*c if a <= b /\ c >= 0
end
spec
OrderedField [DefineOrderedField] =
CommutativeField[DefineCommutativeField]
end
spec
DefineArchimedianField =
DefineOrderedField and Nat
then
sort
Nat < Elem
%% The embedding is determined by overloading of 0,1,+,<
var
x:Elem
. exists n:Nat . x Real
%%then
ops
__! :
Nat -> Nat;
__ ^ __ :
Real × Nat -> Real;
-__ , abs:
Real -> Real;
trunc :
Real -> Nat;
sign :
Real -> Int
vars
n : Nat; r:Real
%% n!:
. 0! = 0
. succ(n)! = succ(n)*n!
%% rn:
. r ^ 0 = 1
. r ^ succ(n) = r * (r ^ n)
%% -r:
. -r = 0-r
%% abs(r):
. abs(r) = r if r >= 0
. abs(r) = -r if r < 0
%% trunc(r):
. trunc(r) <= r
. r < trunc(r)+1
%% sign(r):
. sign(r)=-1 if r<0
. sign(0)=0
. sign(r)=1 if r>0
then
%% Sequences and sequence combinators:
sort
Sequence
preds
isNat,
isInt,
nonZero:
Real;
ops
__ ! __ :
Sequence × Nat -> Real;
constSeq:
Real -> Sequence;
N,0,1,2 :
Sequence ;
__+__,__-__, __*__:
Sequence × Sequence -> Sequence;
__ ^ __ , __/__ ,
__div__,__mod__ :
Sequence × Sequence ->? Sequence;
-__, trunc, sign :
Sequence -> Sequence;
__! :
Sequence ->? Sequence;
partialSums :
Sequence -> Sequence;
ifnz__theN__elsE__ :
Sequence × Sequence × Sequence -> Sequence;
__<__,__ <= __,
__>__,__ >= __,
__==__ :
Sequence × Sequence -> Sequence
vars
n:Nat; r:Real; a,b,c,d:Sequence
. isNat(r) <=> r in Nat
. isInt(r) <=> r in Int
. nonZero(r) <=> not r=0
%% defining the constant sequence r,r,r, ...:
. constSeq(r)!n = r
%% defining the identity sequence 0,1,2,3, ...:
. N!n = n
%% defining the sequences 0= 0, 0, 0, ...,
%% 1=1,1,1 ... and 2 = 2,2,2, ...:
. 0 = constSeq(0)
. 1 = constSeq(1)
. 2 = constSeq(2)
%% add, subtract, multiyply sequences componentwise:
. (a+b)!n = a!n + b!n
. (a-b)!n = a!n - b!n
. (a*b)!n = a!n * b!n
%% power function for sequences:
. def (a ^ b) <=> forall k: Nat . isNat(b!k)
. (a ^ b)!n = a!n ^ (b!n as Nat) if def (a ^ b)
%% devide sequences componentwise:
. def (a/b) <=> forall k: Nat . nonZero(b!k)
. (a/b)!n = a!n / b!n if def a/b
%% div componentwise:
. def (a div b) <=>
forall k:Nat . isInt(a!k) /\ isInt(b!k) /\ nonZero(b!k)
. (a div b)!n = (a!n as Int) div (b!n as Int) if def (a div b)
%% mod componentwise:
. def (a mod b) <=>
forall k:Nat . isInt(a!k) /\ isInt(b!k) /\ nonZero(b!k)
. (a mod b)!n = (a!n as Int) mod (b!n as Int) if def(a mod b)
%% invert all elements of a sequence:
. (-a)!n = -(a!n)
%% trunc:
. trunc(a)!n = trunc(a!n)
%% sign:
. sign(a)!n = sign(a!n)
%% factorial function for sequences:
. def(a!) <=> forall k: Nat . isNat(a!k)
. (a!)!n = (a!n as Nat)! if def (a!)
%% partial sums of a sequence:
%% a!i := a!0 + a!1 + ...+ a!i
. partialSums(a)!0 = a!0
. partialSums(a)!succ(n) = partialSums(a)!n + a!succ(n)
%% if-then-else for sequences:
. (ifnz a theN b elsE c) !n =
b!n when nonZero(a!n) else
c!n
%% comparison functions, 1 represents true, 0 represents false:
. (ab)!n = 1 when a!n > b!n else 0
. (a >= b) !n = 1 when a!n >= b!n else 0
. (a==b)!n = 1 when a!n = b!n else 0
then
%% Polynomials:
pred
__ isZeroAfter __ : Sequence × Nat
vars
s: Sequence; n: Nat
. s isZeroAfter n <=> forall m: Nat . m>n => s!m=0
sort
Polynom = { p:Sequence . exists n:Nat . p isZeroAfter n }
op
degree : Polynom -> Int
var
p:Polynom; n:Nat
. degree(p)=n <=> nonZero(p!n) /\ p isZeroAfter n
. degree(0 as Polynom) = -1
then
%% Convergence, infinite sums, and Cauchy sequences:
ops
lim,sum : Sequence ->? Real
preds
__ -> __ :
Sequence * Real;
converges,isCauchy :
Sequence
vars
r:Real; a:Sequence
%% Convergence of a sequence:
. a->r <=>
forall epsilon:Real . exists n:Nat . forall m:Nat . m >= n => abs(a!m - r) < epsilon
. lim(a)=r <=> a->r
. converges(a) <=> def lim(a)
%% infinite sums:
. sum(a) = lim(partialSums(a))
%% Cauchy sequences:
. isCauchy(a) <=>
forall epsilon:Real . exists n:Nat . forall m,k:Nat . m >= n /\ k >= n => abs(a!m - a!k) < epsilon
then
%% Algebraic closedness of the field:
var
p:Polynom
. odd(degree(p)) => exists x:Real . sum(p * (constSeq(x) ^ N))=0
then
%% completeness axiom:
var
a:Sequence
. chauchy(a) => converges(a)
end
spec
BasicReal[DefineBasicReal] =
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) <=> not exists z: Int . x= (2*z+1) * pi/2
. tan(x) = sin(x) / cos(x) ifdeftan(x)
. defcot(x) <=> not 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
Back to the Basic Datatypes in CASL
Markus Roggenbach last update March 5, 1999.