Rodin Handbook





 

3.3.6 Arithmetic

3.3.6.1 Sets of numbers

$\mathord {\mathbb Z}$

INT

Integers

$\mathord {\mathbb N}$

NAT

Natural numbers, starting with 0

$\mathord {\mathbb N}_1$

NAT1

Natural numbers, starting with 1

$\mathbin {.\mkern 1mu.}$

..

Range of numbers

Description

The set of all integers is denoted by $\mathord {\mathbb Z}$. It contains all elements of the type. The two subsets $\mathord {\mathbb N}$ and $\mathord {\mathbb N}_1$ contain all elements greater than or equal to 0 and 1 respectively. The range of numbers between $\textsf{a}$ and $\textsf{b}$ is denoted by $\textsf{a}\mathbin {.\mkern 1mu.}\textsf{b}$.

Definition

$\mathord {\mathbb N}\mathrel {\widehat=}\{ ~  n ~ |~  n\in \mathord {\mathbb Z}\land n\geq 0~ \} $
$\mathord {\mathbb N}_1 \mathrel {\widehat=}\{ ~  n ~ |~  n\in \mathord {\mathbb Z}\land n\geq 1~ \} $
$\textsf{a}\mathbin {.\mkern 1mu.}\textsf{b}\mathrel {\widehat=}\{ ~  n ~ |~  n\in \mathord {\mathbb Z}\land \textsf{a}\leq n \land n\leq \textsf{b}~ \} $

Types

$\mathord {\mathbb Z}\in \mathop {\mathbb P\hbox{}}\nolimits (\mathord {\mathbb Z})$
$\mathord {\mathbb N}\in \mathop {\mathbb P\hbox{}}\nolimits (\mathord {\mathbb Z})$
$\mathord {\mathbb N}_1\in \mathop {\mathbb P\hbox{}}\nolimits (\mathord {\mathbb Z})$
$\textsf{a}\mathbin {.\mkern 1mu.}\textsf{b}\in \mathop {\mathbb P\hbox{}}\nolimits (\mathord {\mathbb Z})$ with $\textsf{a}\in \mathord {\mathbb Z}$ and $\textsf{b}\in \mathord {\mathbb Z}$

WD

$\mathcal{L}(\mathord {\mathbb Z}) \mathrel {\widehat=}\mathord {\top }$
$\mathcal{L}(\mathord {\mathbb N}) \mathrel {\widehat=}\mathord {\top }$
$\mathcal{L}(\mathord {\mathbb N}_1) \mathrel {\widehat=}\mathord {\top }$
$\mathcal{L}(\textsf{a}\mathbin {.\mkern 1mu.}\textsf{b}) \mathrel {\widehat=}\mathcal{L}(\textsf{a}) \land \mathcal{L}(\textsf{b})$


3.3.6.2 Arithmetic operations

$+$

+

Addition

$-$

-

Subtraction or unary minus

$\cdot $

*

Multiplication

$\div $

/

Integer division

$\bmod $

mod

Modulo

$\mathbin {\widehat{\enskip }}$

^

Exponentiation

Description

These are the usual arithmetic operations.

Definition

Addition, subtraction and multiplication behave as expected.

The division is defined in a way that $1\div 2=0$ and $-1\div 2=0$:
$\textsf{a}\div \textsf{b}= \max (\{ ~ c ~ |~  c\in \mathord {\mathbb N}\land \textsf{b}\cdot c \leq \textsf{a}~ \} )$ for $\textsf{a}\in \mathord {\mathbb N}$ and $\textsf{b}\in \mathord {\mathbb N}$
$(-\textsf{a})\div b = - (\textsf{a}\div b)$
$\textsf{a}\div (-b) = - (\textsf{a}\div b)$

$\textsf{a}\bmod \textsf{b}= c~ \mathrel {\widehat=}~ c\in 0\mathbin {.\mkern 1mu.}\textsf{b}-1 \land \exists k~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ k\in \mathord {\mathbb N}\land k\cdot \textsf{b}+ c = \textsf{a}$

Types

With $\textsf{a}\in \mathord {\mathbb Z}$, $\textsf{b}\in \mathord {\mathbb Z}$ for each operator $\mathbin {\Box }$ of $+$, $-$, $\cdot $, $\div $, $\bmod $:
$\textsf{a}\mathbin {\Box }\textsf{b}\in \mathord {\mathbb Z}$
$-\textsf{a}\in \mathord {\mathbb Z}$

WD

$\mathcal{L}(\textsf{a}+\textsf{b}) \mathrel {\widehat=}\mathcal{L}(\textsf{a}) \land \mathcal{L}(\textsf{b})$
$\mathcal{L}(\textsf{a}-\textsf{b}) \mathrel {\widehat=}\mathcal{L}(\textsf{a}) \land \mathcal{L}(\textsf{b})$
$\mathcal{L}(-\textsf{a}) \mathrel {\widehat=}\mathcal{L}(\textsf{a})$
$\mathcal{L}(\textsf{a}\cdot \textsf{b}) \mathrel {\widehat=}\mathcal{L}(\textsf{a}) \land \mathcal{L}(\textsf{b})$
$\mathcal{L}(\textsf{a}\div \textsf{b}) \mathrel {\widehat=}\mathcal{L}(\textsf{a}) \land \mathcal{L}(\textsf{b}) \land \textsf{b}\neq 0$
$\mathcal{L}(\textsf{a}\bmod \textsf{b}) \mathrel {\widehat=}\mathcal{L}(\textsf{a}) \land \mathcal{L}(\textsf{b}) \land \textsf{a}\geq 0 \land \textsf{b}> 0$
$\mathcal{L}(\textsf{a}\mathbin {\widehat{\enskip }}\textsf{b}) \mathrel {\widehat=}\mathcal{L}(\textsf{a}) \land \mathcal{L}(\textsf{b}) \land \textsf{a}\geq 0 \land \textsf{b}\geq 0$


3.3.6.3 Minimum and Maximum

$\min $

min

Minimum

$\max $

max

Maximum

Description

$\min (\textsf{S})$ and $\max (\textsf{S})$ denotes the smallest and largest number in the set of integers $\textsf{S}$ respectively.

The minimum and maximum are only defined if such a number exists.

Definition

$\min (\textsf{S})\in \textsf{S}\land (\forall x\mathord {\mkern 1mu\cdot \mkern 1mu}x\in \textsf{S}\mathbin \Rightarrow \min (\textsf{S})\leq x)$
$\max (\textsf{S})\in \textsf{S}\land (\forall x\mathord {\mkern 1mu\cdot \mkern 1mu}x\in \textsf{S}\mathbin \Rightarrow \max (\textsf{S})\geq x)$

Types

$\min (\textsf{S})\in \mathord {\mathbb Z}$ and $\max (\textsf{S})\in \mathord {\mathbb Z}$ with $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\mathord {\mathbb Z})$.

WD

$\mathcal{L}(\min (\textsf{S})) \mathrel {\widehat=}\mathcal{L}(\textsf{S}) \land \textsf{S}\neq \emptyset \land \exists b \mathord {\mkern 1mu\cdot \mkern 1mu}\forall x\mathord {\mkern 1mu\cdot \mkern 1mu}x\in \textsf{S}\mathbin \Rightarrow b\leq x$
$\mathcal{L}(\max (\textsf{S})) \mathrel {\widehat=}\mathcal{L}(\textsf{S}) \land \textsf{S}\neq \emptyset \land \exists b \mathord {\mkern 1mu\cdot \mkern 1mu}\forall x\mathord {\mkern 1mu\cdot \mkern 1mu}x\in \textsf{S}\mathbin \Rightarrow b\geq x$