Integers

Uses Logical truth. Requires special terms (integers) that cannot be implemented in Leibniz itself. They are written as standard numerals, e.g. 1 or -2.

The sort ℕ describes the natural numbers. It has two subsorts: zero ⊆ ℕ for the number 0 and ℕ.nz ⊆ ℕ for the non-zero natural numbers. The number 1 has its own subsort as well: one ⊆ ℕ.nz.

The sort ℤ describes the integers. It also has a subsort for its non-zero elements: ℤ.nz ⊆ ℤ.

Since the natural numbers are integers as well, we further have ℕ ⊆ ℤ and ℕ.nz ⊆ ℤ.nz.

Arithmetic

Addition

The sum of two integers is an integer:
 ℤ + ℤ : ℤ

Several special cases for subsorts deserve specific definitions:
 ℕ + ℕ : ℕ
 ℕ.nz + ℕ.nz : ℕ.nz
 ℕ.nz + ℕ : ℕ.nz
 ℕ + ℕ.nz : ℕ.nz

Addition is commutative:
 x:ℤ, y:ℤ, x + y = y + x
and associative:
 x:ℤ, y:ℤ, z:ℤ, (x + y) + z = x + (y + z)

Rules:

Eliminate zeros:
 (x:ℤ) + (zero:zero) ⇒ x
 (zero:zero) + (x:ℤ) ⇒ x

Evaluation for number terms:
 (x:ℤ) + (y:ℤ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x + y"

Subtraction

The difference between two integers is an integer:
 ℤ - ℤ : ℤ

An important special case:
 ℕ.nz - one : ℕ

The negative of an integer is an integer:
 -(ℤ) : ℤ

Rules:

Eliminate zeros:
 (x:ℤ) - (zero:zero) ⇒ x
 (zero:zero) - (x:ℤ) ⇒ -(x)

Evaluation for number terms:
 (x:ℤ) - (y:ℤ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x - y"
 -(x:ℤ) ⇒ Pharo:"x ensureNumber. x negated"

Multiplication

The product of two integers is an integer:
 ℤ × ℤ : ℤ

Important special cases for subsorts:
 ℕ × ℕ : ℕ
 ℕ.nz × ℕ.nz : ℕ.nz
 ℤ.nz × ℤ.nz : ℤ.nz

Multiplication is commutative:
 x:ℤ, y:ℤ, x × y = y × x
and associative:
 x:ℤ, y:ℤ, z:ℤ, (x × y) × z = x × (y × z)

Addition is distributive over multiplication:
 x:ℤ, y:ℤ, z:ℤ, x × (y + z) = (x × y) + (x × z)

Rules:

Eliminate zeros:
 (x:ℤ) × (zero:zero) ⇒ 0
 (zero:zero) × (x:ℤ) ⇒ 0

Eliminate ones:
 (one:one) × (x:ℤ) ⇒ x
 (x:ℤ) × (one:one) ⇒ x

Evaluate for number terms:
 (x:ℤ) × (y:ℤ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x * y"

Division

Integer division yields a quotient:
 ℤ div ℤ.nz : ℤ
and a remainder:
 ℤ rem ℤ.nz : ℤ

Special case for the natural numbers:
 ℕ div ℕ.nz : ℕ
 ℕ rem ℕ.nz : ℕ

Rules:

Eliminate zeros:
 (zero:zero) div (x:ℤ.nz) ⇒ 0
 (zero:zero) rem (x:ℤ.nz) ⇒ 0

Eliminate ones:
 (x:ℤ) div (one:one) ⇒ x
 (x:ℤ) rem (one:one) ⇒ 0

Evaluate for number terms:
 (x:ℤ) div (y:ℤ.nz) ⇒ Pharo:"x ensureNumber. y ensureNumber. x div: y"
 (x:ℤ) rem (y:ℤ.nz) ⇒ Pharo:"x ensureNumber. y ensureNumber. x rem: y"

Exponentiation

Exponentiation is defined for all integers with positive integer powers:
 ℤ^ℕ.nz : ℤ

Special cases for subsorts:
 ℕ^ℕ.nz : ℕ
 ℕ.nz^ℕ.nz : ℕ.nz
 ℤ.nz^ℕ.nz : ℤ.nz

Non-zero integers can also be raised to power zero:
 ℤ.nz^zero : ℕ.nz

Rules:

Eliminate zeros:
 (x:ℤ.nz)^zero:zero ⇒ 1
 (zero:zero)^x:ℕ.nz ⇒ 0

Eliminate ones:
(x:ℤ.nz)^one:one ⇒ x

Evaluate for number terms:
 (x:ℤ)^y:ℕ.nz ⇒ Pharo:"x ensureNumber. y ensureNumber. x raisedTo: y"

Comparison

ℤ < ℤ : 𝔹
ℤ > ℤ : 𝔹
ℤ ≤ ℤ : 𝔹
ℤ ≥ ℤ : 𝔹

Evaluation rules for number terms:
 (x:ℤ) < (y:ℤ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x < y"
 (x:ℤ) > (y:ℤ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x > y"
 (x:ℤ) ≤ (y:ℤ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x <= y"
 (x:ℤ) ≥ (y:ℤ) ⇒ Pharo:"x ensureNumber. y ensureNumber. x >= y"