Rodin User’s Handbook v.2.8: 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 $\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$

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