1. Naturals
1.1 Basics
Introduces: natural , positive-integer , successor _ , 0 .
- 0 : natural .
- successor _ :: natural -> positive-integer (total, injective) .
(1) natural = 0 | positive-integer (disjoint) .
(2) positive-integer = successor natural .
closed.
1.2 Specifics
Introduces: 1 , 2 , 3 , 4 , 5 , 6 , 7 , 8 , 9 ,
_0 , _1 , _2 , _3 , _4 , _5 , _6 , _7 , _8 , _9 ,
sum _ , product _ , exponent _ , integer-quotient _ , integer-remainder _ .
Includes: Instant/Total Order ( natural for s , _ is _ , _ is less than _ ) .
Needs: Tuples/Basics . natural <= component .
- 1 , 2 , 3 , 4 , 5 , 6 , 7 , 8 , 9 : natural .
- _0 , _1 , _2 , _3 , _4 , _5 , _6 , _7 , _8 , _9 :: natural -> natural (total) .
- sum _ :: natural* -> natural (total, associative, commutative, unit is 0) .
- product _ :: natural* -> natural (total, associative, commutative, unit is 1).
- exponent _ :: (natural, natural) -> natural (total).
- integer-quotient _ :: (natural, natural) -> natural (partial) .
- integer-remainder _ :: (natural, natural) -> natural (partial) .
(1) 1 = successor 0 ; 2 = successor 1 ; 3 = successor 2 ;4 = successor 3 ;
5 = successor 4 ; 6 = successor 5 ; 7 = successor 6 ;8 = successor 7 ;
9 = successor 8 ; 10 = successor 9 .
(2) (n:natural)0 = product (n, 10) ;
(n:natural)1 = sum (product (n, 10), 1) ;
...
(n:natural)9 = sum (product (n, 10), 9) .
(3) sum _ :: natural*, positive-integer -> positive-integer ;
sum (n:natural, 1) = successor n .
(4) product _ :: positive-integer* -> positive-integer ;
product (n:natural, 0) = 0 ;
product (m:natural, successor n:natural) = sum (m, product (m,
n)) .
(5) exponent (m:natural, 0) = 1 ;
exponent (m:natural, successor n:natural) = product (m, exponent (m,
n)) .
(6) integer-quotient (n:natural, 0) = nothing ;
integer-remainder (n:natural, 0) = nothing .
(7) m is less than p = true ; m, n : natural ; p : positive-integer =>
(1) integer-quotient (sum (product (n, p), m), p) =
n ;
(2) integer-remainder (sum (product (n, p), m), p) =
m .
(8) 0 is p:positive-integer = false ;
successor m:natural is successor n:natural = m is n .
(9) 0 is less than p:positive-integer = true ; n:natural is less than 0 = false ;
successor m:natural is less than successor n:natural = m is less than
n .
(10)natural [min m:natural] = m | natural [min successor m] (disjoint) ;
natural [max successor m:natural] = natural [max m] | successor
m (disjoint) .
(11)natural [min 0] = natural ; natural [max 0] = 0 .
2. Integers
2.1. Basics
Introduces: integer , negative-integer , nonzero-integer , predecessor _ .
- successor _ :: integer -> integer (total, injective) .
- predecessor _ :: integer -> integer (total, injective) .
(1) integer = 0 | nonzero-integer (disjoint) .
(2) nonzero-integer = positive-integer | negative-integer (disjoint) .
(3) successor _ :: negative-integer -> 0|negative-integer .
(4) predecessor _ :: 0|negative-integer -> negative-integer, positive-integer -> natural .
(5) successor predecessor i:integer = i ; predecessor successor i:integer =
i .
closed.
2.2. Specifics
Introduces: negation _ , absolute _ , difference _ .
Includes: Instant/Total Order ( integer for s , _ is _ , _ is less than _ ) .
Needs: Tuples/Basics . integer <= component .
- negation _ :: integer -> integer (total) .
- absolute _ :: integer -> natural (total) .
- sum _ :: integer* -> integer (total, associative, commutative, unit is 0) .
- difference _ :: (integer, integer) -> integer (total) .
- product _ :: integer* -> integer (total, associative, commutative, unit is 1) .
- exponent _ :: (integer, natural) -> integer (total) .
- integer-quotient _ :: (integer, integer) -> integer (partial) .
- integer-remainder_ :: (integer, integer) -> integer (partial) .
(1) negation 0 = 0 ;
negation successor i:integer = predecessor negation i ;
negation negation i:integer = i ;
negation positive-integer = negative-integer .
(2) absolute n:natural = n ; absolute negation n:natural = n .
(3) sum (i:integer, 1) = successor i ;
sum (i:integer, negation 1) = predecessor i .
(4) difference (i:integer, j:integer) = sum (i, negation j) .
(5) product (0, i:integer) = 0 ;
product (negation i:integer, j:integer) = negation product (i,
j) ;
product (sum (i:integer, j:integer), k:integer) =
sum (product (i, k), product (j,k)) .
(6) exponent (negation i:integer, product (2, n:natural)) =
exponent (i, product (2, n)) .
(7) exponent (negation i:integer, successor product (2, n:natural)) =
negation exponent (i, successor product (2, n)) .
(8) integer-quotient (i:integer, 0) = nothing ;
integer-quotient (negation i:integer, j:integer) =
negation integer-quotient (i, j) ;
integer-quotient (i:integer, negation j:integer) =
negation integer-quotient (i, j) .
(9) integer-remainder (i:integer, 0) = nothing ;
integer-remainder (negation i:integer, j:integer) =
negation integer-remainder (i, j) ;
integer-remainder (i:integer, negation j:integer) = integer-remainder (i,
j) .
(10)i, j : integer => sum (product (integer-quotient (i, j),
j), integer-remainder (i, j)) = i .
(11)m:negative-integer is 0 = false ;
negation i:integer is negation j:integer = i is j ;
m:negative-integer is p:positive-integer = false ;
sum (i:integer, j:integer) is sum (i, k:integer) =
j is k .
(12)m:negative-integer is less than 0 = true ;
negation i:integer is less than negation j:integer = j is less than
i ;
sum (i:integer, j:integer) is less than sum (i, k:integer) =
j is less than k .
(13)integer [min m:integer] = m | integer [min successor m] (disjoint) ;
integer [max successor m:integer] = integer [max m] | successor
m (disjoint) .
3. Rationals
3.1. Basics
Introduces: rational , nonzero-rational , positive-rational , negative-rational , quotient _ .
- quotient _ :: integer, nonzero-integer -> rational (total) .
(1) rational = 0 | nonzero-rational (disjoint) .
(2) nonzero-rational = positive-rational | negative-rational (disjoint).
(3) positive-integer <= positive-rational ; negative-integer <= negative-rational .
(4) quotient _ :: positive-integer, positive-integer ->o positive-rational,
negative-integer, positive-integer -> negative-rational, integer, 0 -> nothing .
(5) quotient (negation i:integer, j:nonzero-integer) = negation quotient (i,
j) .
(6) quotient (i:integer, negation j:nonzero-integer) = negation quotient (i,
j) .
(7) quotient (product (i:nonzero-integer, j:integer), product (i,
k:integer)) =
quotient (j, k) .
(8) quotient (i:integer, 1) = i . quotient (0, i:nonzero-integer) = 0 .
closed.
3.2.
Specifics
Introduces: truncation _ , fraction _ .
Includes: Instant/Total Order ( rational for s , _ is _ , _ is less than _ ) .
Needs: Tuples/Basics . rational <= component .
- quotient _ :: rational, nonzero-rational -> rational (total) .
- truncation _ :: rational -> integer (total) .
- fraction _ :: rational -> rational (total) .
- negation _ :: nonzero-rational -> nonzero-rational (total) .
- absolute _ :: nonzero-rational -> positive-rational (total) .
- sum _ :: rational* -> rational (total, associative, commutative, unit is 0) .
- difference _ :: (rational, rational) -> rational (total) .
- product _ :: rational* -> rational (total, associative, commutative, unit is 1) .
- exponent _ :: (rational, integer) -> rational (partial) .
(1) quotient _ :: positive-rational, positive-rational -> positive-rational,
negative-rational, positive-rational -> negative-rational,
rational, 0 -> nothing .
(2) truncation quotient (i:integer, j:nonzero-integer) = integer-quotient (i,
j) .
(3) fraction quotient (i:integer, j:nonzero-integer) =
quotient (integer-remainder (i, j), j) .
(4) negation quotient (r:rational, n:nonzero-rational) = quotient (negation
r, n) .
(5) absolute p:positive-rational = p ; absolute n:negative-rational = negation
n .
(6) sum (r:rational, quotient (q:rational, n:nonzero-rational)) =
quotient (sum (product (r, n), q), n) .
(7) difference (q:rational, r:rational) = sum (q, negation r) .
(8) product (r:rational, quotient (q:rational, n:nonzero-rational)) =
quotient (product (r, q), n) .
(9) exponent (quotient (q:rational, n:nonzero-rational), i:integer) =
quotient (exponent (q, i), exponent(n, i)) ;
exponent (quotient (q:rational, n:nonzero-rational),
negation p:positive-integer) = exponent (quotient (n, q),
p) .
(10)quotient (r:rational, quotient (q:nonzero-rational, n:nonzero-rational)) =
quotient (product (r, n), q) ;
quotient (quotient (q:rational, n:nonzero-rational), r:nonzero-rational) =
quotient (q, product (n, r)) .
(11)product (p:nonzero-rational, q:rational) is product (p,
r:rational) = q is r .
(12)product (p:positive-rational, q:rational) is less than
product (p, r:rational) = q is less than r .
4. Approximations
4.1.
Generics
Introduces:approximation , min-approximation , max-approximation .
- approximation <= rational .
- min-approximation, max-approximation : approximation .
(1) approximation [min min-approximation] [max max-approximation] = approximation .
open.
4.2.
Basics
Introduces: interval_ , approximately _ .
- interval _ :: rational -> rational (strict) .
- approximately _ :: rational -> rational (strict, linear) .
The sort interval r
is the smallest closed subsort of rational that includes the sort r,
whereas approximately r is an interval whose bounds are of sort approximation,
or nothing when r is entirely outside the interval from min-approximation
to max-approximation.
(1) r <= rational => r <= interval r .
(2) s, t : r <= rational => rational [min s] [max t] <= interval
r .
(3) x : rational => x : approximately x .
(4) x : rational => interval approximately x = approximately x .
(5) x : approximation => approximately x = x .
(6) x : interval y ; y => approximation => approximately x <= interval
y .
(7) x is greater than max-approximation = true => approximately x:rational = nothing .
(8) x is less than min-approximation = true => approximately x:rational = nothing .
|