Go backward to 4.2 Some Algebraic Specifications
Go up to 4 A Specification of Real Numbers
Go forward to 4.4 The Specification BasicReal

## 4.3 The Specification DefineBasicReal

spec
DefineBasicReal =
Rat
then
sort
Rat < Real
%%
then
ArchimedianField[DefineArchimedianField] with Elem |-> 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 e Nat
.
isInt(r) <=> r e Int
.
nonZero(r) <=> ¬ 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)
%%
.
(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:
.
(a<b)!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
.
(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 . epsilon > 0 => (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 . epsilon >0 => ( 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
.
cauchy(a) => converges(a)
end

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