User Manual for Rodin v.2.3: Arithmetic

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 $a$ and $b$ is denoted by $a \mathbin {.\mkern 1mu.}b$ .
Definition: $\mathord {\mathbb N}= \{ ~ n ~ |~ n\in \mathord {\mathbb Z}\land n\geq 0~ \}$
$\mathord {\mathbb N}_1 = \{ ~ n ~ |~ n\in \mathord {\mathbb Z}\land n\geq 1~ \}$
$a\mathbin {.\mkern 1mu.}b = \{ ~ n ~ |~ n\in \mathord {\mathbb Z}\land a\leq n \land n\leq 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})$
$a \mathbin {.\mkern 1mu.}b\in \mathop {\mathbb P\hbox{}}\nolimits (\mathord {\mathbb Z})$ with $a\in \mathord {\mathbb Z}$ and $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}(a \mathbin {.\mkern 1mu.}b) \mathrel {\widehat=}\mathcal{L}(a) \land \mathcal{L}(b)$

3.3.6.2 Arithmetic operations

$+$	`+`	Addition
$-$	`-`	Subtraction or unary minus
$\cdot$	`*`	Multiplication
$\div$	`/`	Integer division
$\bmod$	`mod`	Modulo
$\mathbin {\widehat{\enskip }}$	`^`	Exponentation

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$ :
$a\div b = \max (\{ ~ c ~ |~ c\in \mathord {\mathbb N}\land b\cdot c \leq a~ \} )$ for $a\in \mathord {\mathbb N}$ and $b\in \mathord {\mathbb N}$
$(-a)\div b = - (a\div b)$
$a\div (-b) = - (a\div b)$

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

Types

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

WD

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

3.3.6.3 Minimum and Maximum

$\min$	`min`	Minimum
$\max$	`max`	Maximum

Description

$\min (I)$ resp. $\max (I)$ denotes the smallest resp. largest number in the set of integers $I$ .

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

Definition

$\min (I) = b \mathrel {\widehat=}b\in I \land (\forall x\mathord {\mkern 1mu\cdot \mkern 1mu}x\in I\mathbin \Rightarrow b\leq x)$
$\max (I) = b \mathrel {\widehat=}b\in I \land (\forall x\mathord {\mkern 1mu\cdot \mkern 1mu}x\in I\mathbin \Rightarrow b\geq x)$

Types

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

WD

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

Rodin Handbook

3.3.6 Arithmetic

3.3.6.1 Sets of numbers

3.3.6.2 Arithmetic operations

3.3.6.3 Minimum and Maximum