# Arithmetic Rewrite Rules

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Rules that are marked with a * in the first column are implemented in the latest version of Rodin. Rules without a * are planned to be implemented in future versions. Other conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Rewrite_Rules.

Name Rule Side Condition A/M
*
SIMP_SPECIAL_MOD_0
$0 \,\bmod\, E \;\;\defi\;\; 0$ A
*
SIMP_SPECIAL_MOD_1
$E \,\bmod\, 1 \;\;\defi\;\; 0$ A
*
SIMP_MIN_SING
$\min (\{ E\} ) \;\;\defi\;\; E$ where $E$ is a single expression A
*
SIMP_MAX_SING
$\max (\{ E\} ) \;\;\defi\;\; E$ where $E$ is a single expression A
*
SIMP_MIN_NATURAL
$\min (\nat ) \;\;\defi\;\; 0$ A
*
SIMP_MIN_NATURAL1
$\min (\natn ) \;\;\defi\;\; 1$ A
*
SIMP_MIN_BUNION_SING
$\begin{array}{cl} & \min (S \bunion \ldots \bunion \{ \min (T)\} \bunion \ldots \bunion U) \\ \defi & \min (S \bunion \ldots \bunion T \bunion \ldots \bunion U) \\ \end{array}$ A
*
SIMP_MAX_BUNION_SING
$\begin{array}{cl} & \max (S \bunion \ldots \bunion \{ \max (T)\} \bunion \ldots \bunion U) \\ \defi & \max (S \bunion \ldots \bunion T \bunion \ldots \bunion U) \\ \end{array}$ A
*
SIMP_MIN_UPTO
$\min (E \upto F) \;\;\defi\;\; E$ A
*
SIMP_MAX_UPTO
$\max (E \upto F) \;\;\defi\;\; F$ A
*
SIMP_LIT_MIN
$\min (\{ E, \ldots , i, \ldots , j, \ldots , H\} ) \;\;\defi\;\; \min (\{ E, \ldots , i, \ldots , H\} )$ where $i$ and $j$ are literals and $i \leq j$ A
*
SIMP_LIT_MAX
$\max (\{ E, \ldots , i, \ldots , j, \ldots , H\} ) \;\;\defi\;\; \max (\{ E, \ldots , i, \ldots , H\} )$ where $i$ and $j$ are literals and $i \geq j$ A
*
SIMP_SPECIAL_CARD
$\card (\emptyset ) \;\;\defi\;\; 0$ A
*
SIMP_CARD_SING
$\card (\{ E\} ) \;\;\defi\;\; 1$ where $E$ is a single expression A
*
SIMP_SPECIAL_EQUAL_CARD
$\card (S) = 0 \;\;\defi\;\; S = \emptyset$ A
*
SIMP_CARD_POW
$\card (\pow (S)) \;\;\defi\;\; 2\expn{\card(S)}$ A
*
SIMP_CARD_BUNION
$\card (S \bunion T) \;\;\defi\;\; \card (S) + \card (T) - \card (S \binter T)$ A
SIMP_CARD_SETMINUS
$\card(S\setminus T)\;\;\defi\;\;\card(S) - \card(T)$ with hypotheses $T\subseteq S$ and either $\finite(S)$ or $\finite(T)$ A
SIMP_CARD_SETMINUS_SETENUM
$\card(S\setminus\{E_1,\ldots,E_n\})\;\;\defi\;\;\card(S) - \card(\{E_1,\ldots,E_n\})$ with hypotheses $E_i\in S$ for all $i\in 1\upto n$ A
*
SIMP_CARD_CONVERSE
$\card (r^{-1} ) \;\;\defi\;\; \card (r)$ A
*
SIMP_CARD_ID
$\card (\id) \;\;\defi\;\; \card (S)$ where $\id$ has type $\pow (S \cprod S)$ A
*
SIMP_CARD_ID_DOMRES
$\card (S\domres\id) \;\;\defi\;\; \card (S)$ A
*
SIMP_CARD_PRJ1
$\card (\prjone) \;\;\defi\;\; \card (S \cprod T)$ where $\prjone$ has type $\pow(S \cprod T \cprod S)$ A
*
SIMP_CARD_PRJ2
$\card (\prjtwo) \;\;\defi\;\; \card (S \cprod T)$ where $\prjtwo$ has type $\pow(S \cprod T \cprod T)$ A
*
SIMP_CARD_PRJ1_DOMRES
$\card (E \domres \prjone) \;\;\defi\;\; \card (E)$ A
*
SIMP_CARD_PRJ2_DOMRES
$\card (E \domres \prjtwo) \;\;\defi\;\; \card (E)$ A
*
SIMP_CARD_LAMBDA
$\card(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \card(\{x\qdot P\mid E\} )$ where $E$ is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., $E$ is syntactically injective) and all identifiers bound by the comprehension set that occur in $F$ also occur in $E$ A
*
SIMP_LIT_CARD_UPTO
$\card (i \upto j) \;\;\defi\;\; j-i+1$ where $i$ and $j$ are literals and $i \leq j$ A
SIMP_TYPE_CARD
$\card (\mathit{Tenum}) \;\;\defi\;\; N$ where $\mathit{Tenum}$ is a carrier set containing $N$ elements A
*
SIMP_LIT_GE_CARD_1
$\card (S) \geq 1 \;\;\defi\;\; \lnot\, S = \emptyset$ A
*
SIMP_LIT_LE_CARD_1
$1 \leq \card (S) \;\;\defi\;\; \lnot\, S = \emptyset$ A
*
SIMP_LIT_LE_CARD_0
$0 \leq \card (S) \;\;\defi\;\; \btrue$ A
*
SIMP_LIT_GE_CARD_0
$\card (S) \geq 0 \;\;\defi\;\; \btrue$ A
*
SIMP_LIT_GT_CARD_0
$\card (S) > 0 \;\;\defi\;\; \lnot\, S = \emptyset$ A
*
SIMP_LIT_LT_CARD_0
$0 < \card (S) \;\;\defi\;\; \lnot\, S = \emptyset$ A
*
SIMP_LIT_EQUAL_CARD_1
$\card (S) = 1 \;\;\defi\;\; \exists x \qdot S = \{ x\}$ A
*
SIMP_CARD_NATURAL
$\card (S) \in \nat \;\;\defi\;\; \btrue$ A
*
SIMP_CARD_NATURAL1
$\card (S) \in \natn \;\;\defi\;\; \lnot\, S = \emptyset$ A
*
SIMP_LIT_IN_NATURAL
$i \in \nat \;\;\defi\;\; \btrue$ where $i$ is a non-negative literal A
*
SIMP_SPECIAL_IN_NATURAL1
$0 \in \natn \;\;\defi\;\; \bfalse$ A
*
SIMP_LIT_IN_NATURAL1
$i \in \natn \;\;\defi\;\; \btrue$ where $i$ is a positive literal A
*
SIMP_LIT_UPTO
$i \upto j \;\;\defi\;\; \emptyset$ where $i$ and $j$ are literals and $j < i$ A
*
SIMP_LIT_IN_MINUS_NATURAL
$-i \in \nat \;\;\defi\;\; \bfalse$ where $i$ is a positive literal A
*
SIMP_LIT_IN_MINUS_NATURAL1
$-i \in \natn \;\;\defi\;\; \bfalse$ where $i$ is a non-negative literal A
*
DEF_IN_NATURAL
$x \in \nat \;\;\defi\;\; 0 \leq x$ M
*
DEF_IN_NATURAL1
$x \in \natn \;\;\defi\;\; 1 \leq x$ M
*
SIMP_LIT_EQUAL_KBOOL_TRUE
$\bool (P) = \True \;\;\defi\;\; P$ A
*
SIMP_LIT_EQUAL_KBOOL_FALSE
$\bool (P) = \False \;\;\defi\;\; \lnot\, P$ A
DEF_EQUAL_MIN
$E = \min (S) \;\;\defi\;\; E \in S \land (\forall x \qdot x \in S \limp E \leq x)$ where $x$ non free in $S, E$ M
DEF_EQUAL_MAX
$E = \max (S) \;\;\defi\;\; E \in S \land (\forall x \qdot x \in S \limp E \geq x)$ where $x$ non free in $S, E$ M
*
SIMP_SPECIAL_PLUS
$E + \ldots + 0 + \ldots + F \;\;\defi\;\; E + \ldots + F$ A
*
SIMP_SPECIAL_MINUS_R
$E - 0 \;\;\defi\;\; E$ A
*
SIMP_SPECIAL_MINUS_L
$0 - E \;\;\defi\;\; -E$ A
*
SIMP_MINUS_MINUS
$- (- E) \;\;\defi\;\; E$ A
*
SIMP_MINUS_UNMINUS
$E - (- F) \;\;\defi\;\; E + F$ where $(-F)$ is a unary minus expression or a negative literal M
*
SIMP_MULTI_MINUS
$E - E \;\;\defi\;\; 0$ A
*
SIMP_MULTI_MINUS_PLUS_L
$(A + \ldots + C + \ldots + B) - C \;\;\defi\;\; A + \ldots + B$ M
*
SIMP_MULTI_MINUS_PLUS_R
$C - (A + \ldots + C + \ldots + B) \;\;\defi\;\; -(A + \ldots + B)$ M
*
SIMP_MULTI_MINUS_PLUS_PLUS
$(A + \ldots + E + \ldots + B) - (C + \ldots + E + \ldots + D) \;\;\defi\;\; (A + \ldots + B) - (C + \ldots + D)$ M
*
SIMP_MULTI_PLUS_MINUS
$(A + \ldots + D + \ldots + (C - D) + \ldots + B) \;\;\defi\;\; A + \ldots + C + \ldots + B$ M
*
SIMP_MULTI_ARITHREL_PLUS_PLUS
$A + \ldots + E + \ldots + B < C + \ldots + E + \ldots + D \;\;\defi\;\; A + \ldots + B < C + \ldots + D$ where the root relation ($<$ here) is one of $\{=, <, \leq, >, \geq\}$ M
*
SIMP_MULTI_ARITHREL_PLUS_R
$C < A + \ldots + C \ldots + B \;\;\defi\;\; 0 < A + \ldots + B$ where the root relation ($<$ here) is one of $\{=, <, \leq, >, \geq\}$ M
*
SIMP_MULTI_ARITHREL_PLUS_L
$A + \ldots + C \ldots + B < C \;\;\defi\;\; A + \ldots + B < 0$ where the root relation ($<$ here) is one of $\{=, <, \leq, >, \geq\}$ M
*
SIMP_MULTI_ARITHREL_MINUS_MINUS_R
$A - C < B - C \;\;\defi\;\; A < B$ where the root relation ($<$ here) is one of $\{=, <, \leq, >, \geq\}$ M
*
SIMP_MULTI_ARITHREL_MINUS_MINUS_L
$C - A < C - B \;\;\defi\;\; B < A$ where the root relation ($<$ here) is one of $\{=, <, \leq, >, \geq\}$ M
*
SIMP_SPECIAL_PROD_0
$E * \ldots * 0 * \ldots * F \;\;\defi\;\; 0$ A
*
SIMP_SPECIAL_PROD_1
$E * \ldots * 1 * \ldots * F \;\;\defi\;\; E * \ldots * F$ A
*
SIMP_SPECIAL_PROD_MINUS_EVEN
$(-E) * \ldots * (-F) \;\;\defi\;\; E * \ldots * F$ if an even number of $-$ A
*
SIMP_SPECIAL_PROD_MINUS_ODD
$(-E) * \ldots * (-F) \;\;\defi\;\; -(E * \ldots * F)$ if an odd number of $-$ A
*
SIMP_LIT_MINUS
$- (i) \;\;\defi\;\; (-i)$ where $i$ is a literal A
*
SIMP_LIT_EQUAL
$i = j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation)$ where $i$ and $j$ are literals A
*
SIMP_LIT_LE
$i \leq j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation)$ where $i$ and $j$ are literals A
*
SIMP_LIT_LT
$i < j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation)$ where $i$ and $j$ are literals A
*
SIMP_LIT_GE
$i \geq j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation)$ where $i$ and $j$ are literals A
*
SIMP_LIT_GT
$i > j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation)$ where $i$ and $j$ are literals A
*
SIMP_DIV_MINUS
$(- E) \div (-F) \;\;\defi\;\; E \div F$ A
*
SIMP_SPECIAL_DIV_1
$E \div 1 \;\;\defi\;\; E$ A
*
SIMP_SPECIAL_DIV_0
$0 \div E \;\;\defi\;\; 0$ A
*
SIMP_SPECIAL_EXPN_1_R
$E ^ 1 \;\;\defi\;\; E$ A
*
SIMP_SPECIAL_EXPN_1_L
$1 ^ E \;\;\defi\;\; 1$ A
*
SIMP_SPECIAL_EXPN_0
$E ^ 0 \;\;\defi\;\; 1$ A
*
SIMP_MULTI_LE
$E \leq E \;\;\defi\;\; \btrue$ A
*
SIMP_MULTI_LT
$E < E \;\;\defi\;\; \bfalse$ A
*
SIMP_MULTI_GE
$E \geq E \;\;\defi\;\; \btrue$ A
*
SIMP_MULTI_GT
$E > E \;\;\defi\;\; \bfalse$ A
*
SIMP_MULTI_DIV
$E \div E \;\;\defi\;\; 1$ A
*
SIMP_MULTI_DIV_PROD
$(X * \ldots * E * \ldots * Y) \div E \;\;\defi\;\; X * \ldots * Y$ A
*
SIMP_MULTI_MOD
$E \,\bmod\, E \;\;\defi\;\; 0$ A
DISTRI_PROD_PLUS
$a * (b + c) \;\;\defi\;\; (a * b) + (a * c)$ M
DISTRI_PROD_MINUS
$a * (b - c) \;\;\defi\;\; (a * b) - (a * c)$ M
DERIV_NOT_EQUAL
$\lnot E = F \;\;\defi\;\; E < F \lor E > F$ $E$ and $F$ must be of Integer type M