4.3 The Specification DefineBasicReal

spec

 DefineBasicReal =

Rat

then

sort

Rat < Real

%%

The embedding is determined by overloading of 0,1,+,_,*,/

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!

%%

rⁿ:

.

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)

%%

add, subtract, multiply 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:

.

(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