5.3 The Specification of the Reals in Higher-Order CASL

We here rely on higher-order CASL as proposed in [HKBM98]. We give two specifications of the reals in higher-order CASL, one using sequences, as BasicReal, and the other one using bounded sets. Both specifications are equivalent.

spec

 DefineHigherOrderReal1 =

Nat and OrderedField with Elem ^_|-> Real

then

ops

__ < __:	pred(Real × pred(Real));
__ < __:	pred(pred(Real) × Real);
isBounded:	pred(pred(Real));
__ < __:	pred(Real × (Nat -> Real));
__ < __:	pred((Nat -> Real × Real);
isBounded:	pred(Nat -> Real)

vars

r,s:Real; M:pred(Real); a:Nat -> Real

.

M < r <=> forall s:Real . M(s) => s < r

.

r < M <=> forall s:Real . M(s) => r < s

.

isBounded(M) <=> exists ub,lb:Real . lb < M /\ M < ub

.

a < r <=> forall n:Nat . a(n) < r

.

r < a <=> forall n:Nat . r < a(n)

.

isBounded(a) <=> exists ub,lb:Real . lb < a /\ a < ub

%%

weak choice:

.

¬ isBounded(M) => exists a:Nat -> Real. ¬ isBounded(a) /\ forall n:Nat. M(a(n))

then

ops

partialSums : (Nat -> Real) -> Nat -> Real

vars

n:Nat; r:Real; a:Nat -> Real

.

partialSums(a)(0) = a(0)

.

partialSums(a)(succ(n)) = partialSums(a)(n) + a(succ(n))

%%

Convergence, infinite sums, and Cauchy sequences:

ops

lim,sum : Nat -> Real ->? Real

preds

__ -> __ :	(Nat -> Real) × Real;
converges,cauchy :	Nat -> Real

vars

r:Real; a:Nat -> Real

%%

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:

.

cauchy(a) <=>	forall epsilon:Real . epsilon > 0 =>
	(exists n:Nat . forall m,k:Nat .
	m > n /\ k > n => abs(a(m) - a(k)) < epsilon )

then

%%

completeness axiom:

var

a:Nat -> Real

.

cauchy(a) => converges(a)

end

spec

 DefineHigherOrderReal2 =

OrderedField with Elem ^_|-> Real

then

ops

__ < __:	pred(Real × pred(Real));
__ < __:	pred(pred(Real) × Real);
isBounded:	pred(pred(Real));
inf,sup :	pred(Real) ->? Real

vars

r,s:Real; M:pred(Real)

.

M < r <=> forall s:Real . M(s) => s < r

.

r < M <=> forall s:Real . M(s) => r < s

.

inf(M)=r <=> r < M /\ forall s:Real . s < M => s < r

.

sup(M)=r <=> M < r /\ forall s:Real . M < s => r < s

.

isBounded(M) <=> exists ub,lb:Real . lb < M /\ M < ub

%%

completeness:

.

isBounded(M) => def inf(M) /\ def sup(M)

end