Numbers
spec
GenerateNat =
free
types
Nat ::= 0 | sort Pos;
Pos ::= suc(pre: Nat)
%% intended system of representatives:
%% sucn(0),
%% where n >= 0 is a natural number, and
%% suc0(0) := 0,
%% sucn+1(0):= suc(sucn(0)).
end
spec
Nat =
GenerateNat with sorts Nat, Pos, ops 0, suc, pre
then
SigOrder
with
sort
Elem |-> Nat,
preds
__ <= __,__ >= __,__<__,__>__
then
ops
+__,
abs: Nat -> Nat;
__ + __,
__ * __,
__ ^ __,
min, max: Nat × Nat -> Nat;
__ - __,
__ div __,
__ mod __: Nat × Nat ->? Nat;
1,2,3,4,5,6,7,8,9: Nat;
__ :: __ : Nat × Nat -> Nat %%left assoc
%%prec __ + __, __ - __ < __ * __, __ div __, __ mod __
%%prec __*__, __div__, __mod__ < __ ^ __
vars
m,n,r: Nat; p: Pos
%% x <= y:
. 0 <= n
. not (p <= 0)
. suc(m) <= suc(n) <=> m <= n
%% + unary:
. + n = n
%% absolute value abs:
. abs(n) = n
%% + binary:
. 0 + m = m
. suc(n) + m = suc(n + m)
%% multiplication:
. 0 * m = 0
. suc(m) * n = n + (m * n)
%% x ^ y:
. m ^ 0 = suc(0)
. m ^ suc(n) = (m ^ n) * m
%% minimum of two numbers:
. min(m,n) = m if m <= n
. min(m,n) = n if m > n
%% maximum of two numbers:
. max(m,n) = m if m >= n
. max(m,n) = n if m < n
%% partially defined additive inverse:
. def (m-n) <=> m >= n
. m - 0 = 0
. suc(m) - suc(n) = m - n if def (suc(m) - suc(n))
%% division:
. def (m div n) <=> n in Pos
. m div n = r if def (m div n) /\
(exists s: Nat . m = n*r + s /\ 0 <= s /\ s < n)
%% rest of division:
. def (m mod n) <=> n in Pos
. m mod n = r if def (m mod n) /\
(exists s: Nat . m = n*s + r /\ 0 <= r /\ r < n)
%% representing the natural numbers with digits:
. 1 = suc (0)
. 2 = suc (1)
. 3 = suc (2)
. 4 = suc (3)
. 5 = suc (4)
. 6 = suc (5)
. 7 = suc (6)
. 8 = suc (7)
. 9 = suc (8)
. m :: n = (m * suc(9)) + n
then
%%cons
var
r,s,t: Nat
%% distributive laws:
. (r + s) * t = (r * t) + (s * t)
. t * (r + s) = (t* r ) + (t * s)
end
view
CommutativeMonoid_in_Nat_Add:
CommutativeMonoid
to Nat =
sort
Elem |-> Nat,
ops
0 |-> 0,
__+__ |-> __+__
end
view
CommutativeMonoid_in_Nat_Mult:
CommutativeMonoid
to Nat =
sort
Elem |-> Nat,
ops
0 |-> 1,
__+__ |-> __*__
end
view
TotalOrder_in_Nat:
TotalOrder
to Nat =
sort
Elem |-> Nat,
pred
__ <= __ |-> __ <= __
end
spec
DefineEuclidianRing =
DefineIntegralDomain with sort Elem, ops 0, 1, __+__, __ * __
and {Nat reveal pred __ < __}
then
op
delta: Elem -> Nat
vars
a,b: Elem
. exists q,r : Elem . a = q * b + r /\
(r = 0 \/ delta(r) < delta(b) ) if ( not b=0
)
end
spec
EuclidianRing
[DefineEuclidianRing with
sorts Elem, Nat,
pred __ < __,
ops 0, 1, __+__, __ * __
] =
IntegralDomain [DefineIntegralDomain]
with
sorts RUnit, Irred,
ops inv, __ - __
end
spec
GenerateInt =
GenerateNat with sorts Nat, Pos, ops 0, suc, pre
then
free
types
Int ::= sort Nat | sort Neg;
Neg ::= -__ (Pos)
%% intended system of representatives:
%% sucn(0), n>0,
%% 0, and
%% -sucn(0), n>0.
ops suc,
pre: Int -> Int
var
p:Pos
%% in GenerateNat the operations suc and pre are defined as
%% suc: Nat -> Nat and pre: Pos -> Nat
%% here we augment them to total operations of type Int -> Int;
%% suc:
. suc(-p) = -pre(p)
%% pre:
. pre(0) = -suc(0)
. pre(-p) = -suc(p)
end
spec
Int =
GenerateInt with sorts Nat, Pos, Neg, ops 0, suc, pre
and Nat
hide ops __ - __ %% ops added before __ - __
with preds __ <= __,__ >= __,__<__,__>__,
ops +__, abs, __ + __, __ * __,
__ div __, __ mod __, min, max, __ ^ __,
1,2,3,4,5,6,7,8,9, __ :: __
then
preds
odd: Int;
even: Int;
ops
+__,
-__: Int -> Int;
abs: Int -> Nat;
__ + __,
__ - __,
__ * __,
min, max,
__^ __: Int × Nat -> Int;
__ / __,
__ div __,
__ mod __,
__ quot __,
__ rem __: Int × Int ->? Int;
%%prec __ + __, __ - __ < __ * __, __ div __, __ mod __
%%prec __ * __, __ div __, __ mod __ < __^ __
vars
m,n: Nat; p,q: Pos; x,y,z: Int %% inserted ; between Nat and q
%% x <= y for -Pos:
. -p <= n
. not (m <= -p)
. -p <= -q <=> q <= p
%% even and odd:
. even(0)
. not odd(0)
. odd(suc(m)) <=> even(m)
. even(suc(m)) <=> odd(m)
. even(-p) <=> even(p)
. odd(-p) <=> odd(p)
%% unary + for -Pos:
. + (-p) = -p
%% unary - for 0 and -Pos:
. -0 = 0
. - (- p) = p
%% abs(x) for -Pos:
. abs(-p)=p
%% binary + for -Pos:
. 0 + (-p) = -p
. (-p) + 0 = -p
. suc(m) + (-p) = m + suc(-p)
. (-p) + suc(m) = suc(-p) + m
. (-p) + (-q) = - (p + q)
%% binary -:
. x - y = x + (-y)
%% Multiplication for -__(Pos):
. 0 * (-p) = 0
. (-p) * 0 = 0
. (-p) * (-q) = p * q
. (-p) * q = - (p * q)
. p * (-q) = - (p * q)
%% min(x,y) - new definition:
. min(x,y) = x if x <= y
. min(x,y) = y if x > y
%% max(x,y) - new definition:
. max(x,y) = y if x <= y
. max(x,y) = x if x > y
%% power(x ^ n) for -__(Pos):
. (-p) ^ 0 = suc(0)
. (-p) ^ suc(n) = ((-p) ^ n) * (-p)
%% "ordinary" division:
. def x/y <=> exists t: Int . y * t = x
. (x/y = z <=> z*y = x) if def x/y
%% div - new definition:
. def x div y <=> not y = 0
. x div y = z if def (x mod y) /\
(exists r: Int . x = y*z + r /\ 0 <= r /\ r <
abs(y))
%% mod - new definition:
. def x mod y <=> not y = 0
. x mod y = z if def (x mod y) /\
(exists s: Int . x = y*s + z /\ 0 <= z /\ z <
abs(y))
%% quot:
. def x quot y <=> not y = 0
. x quot y = abs(x) ÷abs(y) if def (x quot y) /\
((x >= 0 /\ y > 0) \/ (x <= 0 /\ y < 0))
. x quot y = - (abs(x) div abs(y)) if def (x quot y) /\
((x >= 0 /\ y < 0) \/ (x <= 0 /\ y > 0))
%% rem:
. def x rem y <=> not y = 0
. x rem y = abs(x) mod abs(y) if def (x rem y) /\ x >= 0
. x rem y = - (abs(x) mod abs(y)) if def (x rem y) /\ x < 0
end
view
EuclidianRing_in_Int: DefineEuclidianRing to Int =
%% Signature of DefineIntegralDomain:
sort
Elem |-> Int,
ops
0 |-> 0,
1 |-> 1,
__ + __ |-> __ + __ ,
__ * __ |-> __ * __, %% at this place a comma added
%% Nat is a subsort of Int
op
delta |-> abs
end
view
TotalOrder_in_Int:
TotalOrder
to Int =
sort
Elem |-> Int,
pred
__ <= __ |-> __ <= __
end
spec
GenerateRat =
Int
hide op __ / __
with
sorts Nat, Pos, Neg, Int,
preds __ <= __,__ >= __,__<__,__>__,
odd, even,
ops 0, suc, pre,
+__, -__, abs, __ + __, __-__, __ * __,
min, max, __ ^ __,
__ div __, __ mod __, __ quot __, __ rem __,
1,2,3,4,5,6,7,8,9, __ :: __
then
free
{
type
Rat ::= sort Int | __ / __ (nom: Int ; denom: Pos)
vars
i,j: Int; p,q: Pos
%% embedding Int in Rat:
. i/1 = i
%% equality of rational numbers:
. i/p = j/q <=> i*q = j*p
}
%% intended system of representatives:
%% i and
%% j / p,
%% where i,j are of sort Int, p > 1 is of sort Pos,
%% and for any pair j/p holds: j and p are relatively prime.end
spec
Rat =
GenerateRat with
sorts Nat, Pos, Neg, Int, Rat,
preds __ <= __,__ >= __,__<__,__>__,
odd, even,
ops 0, suc, pre,
+__, -__, abs, __ + __, __-__, __ * __, __ / __,
__ div __, __ mod __, min, max, __ ^ __,
1,2,3,4,5,6,7,8,9, __ :: __
then
Sig_Order
with preds __ <= __,__ >= __,__<__,__>__,
sorts Elem |-> Rat
then
ops
+ __ ,
- __ : Rat -> Rat;
__ + __ ,
__ - __ ,
__ * __ : Rat × Rat -> Rat;
__ / __ : Rat × Rat ->? Rat;
%%prec __ + __, __ - __ < __ * __, __ / __
%% operations for a representation of Rat as decimal fraction :
ops
__ ::: __ : Nat × Nat -> Rat;
__ E __ : Rat × Int -> Rat
%%prec __ E __ < __ ::: __
vars
m,n: Nat; r,s: Rat
%% + unary:
. + r = r
%% - unary:
. - r = (-nom(r)) / denom(r)
%% +, -, *:
. r+s = (nom(r) * denom(s) + nom(s)* denom(r))/ (denom(r) *
denom(s))
. r-s = (nom(r) * denom(s) - nom(s)* denom(r))/ (denom(r) *
denom(s))
. r*s = (nom(r) * nom(s)) / ( denom(r) * denom(s) )
%% partial function /:
. def r/s <=> not (s = 0)
. r/s = ((nom(r) * denom(s)) / (denom(r) * nom(s)))
if ( def (r/s) /\ nom(s) >= 0 )
. r/s = ( -1 * (nom(r) * denom(s))) / ( -1 * denom(r) * nom(s))
if ( def (r/s) /\ nom(s) < 0 )
%% ordering:
. r <= s <=> nom(r)*denom(s) <= nom(s) * denom(r)
then local
op
tenPower: Nat -> Nat;
vars
n,m: Nat
%% tenPower(n):= min { 10k | k in N \{0}, 10k > n }:
. tenPower(n)=10 if n < 10
. tenPower( ((1::0) * m) + n)= (1::0) * tenPower(m) if n < (1::0)
within
vars
n,m: Nat; p: Pos
%% represent the floating point number n.m as rational:
. n:::m = n + (m/tenPower(m))
%% introduce an exponent:
. r E n = r* ((1::0) ^ n)
. r E (-p) = r / ((1::0) ^ n)
end
view
CommutativeField_in_Rat:
DefineCommutativeField to Rat =
sorts
Elem |-> Rat,
ops
0 |-> 0,
1 |-> 1,
__+__ |-> __+__,
__*__ |-> __*__
end
view
TotalOrder_in_Rat:
TotalOrder
to Rat =
sort
Elem |-> Rat,
pred
__ <= __ |-> __ <= __
end
Back to the Basic Datatypes in CASL
Markus Roggenbach last update March 5, 1999.