Difference between pages "Adding Reasoners(How to extend Rodin Tutorial)" and "All Rewrite Rules"

Revision as of 16:15, 11 February 2009

This page groups together all the rewrite rules implemented (or planned for implementation) in the Rodin prover. The rules themselves can be found in the following locations (for editing purposes):

Conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Rewrite_rules

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_AND_BTRUE	$P \land \ldots \land \btrue \land \ldots \land Q \;\;\defi\;\; P \land \ldots \land Q$		A
*	SIMP_SPECIAL_AND_BFALSE	$P \land \ldots \land \bfalse \land \ldots \land Q \;\;\defi\;\; \bfalse$		A
*	SIMP_MULTI_AND	$P \land \ldots \land Q \land \ldots \land Q \land \ldots \land R \;\;\defi\;\; P \land \ldots \land Q \land \ldots \land R$		A
*	SIMP_MULTI_AND_NOT	$P \land \ldots \land Q \land \ldots \land \lnot\, Q \land \ldots \land R \;\;\defi\;\; \bfalse$		A
*	SIMP_SPECIAL_OR_BTRUE	$P \lor \ldots \lor \btrue \lor \ldots \lor Q \;\;\defi\;\; \btrue$		A
*	SIMP_SPECIAL_OR_BFALSE	$P \lor \ldots \lor \bfalse \lor \ldots \lor Q \;\;\defi\;\; P \lor \ldots \lor Q$		A
*	SIMP_MULTI_OR	$P \lor \ldots \lor Q \lor \ldots \lor Q \lor \ldots \lor R \;\;\defi\;\; P \lor \ldots \lor Q \lor \ldots \lor R$		A
*	SIMP_MULTI_OR_NOT	$P \lor \ldots \lor Q \lor \ldots \lor \lnot\, Q \land \ldots \land R \;\;\defi\;\; \btrue$		A
*	SIMP_SPECIAL_IMP_BTRUE_R	$P \limp \btrue \;\;\defi\;\; \btrue$		A
*	SIMP_SPECIAL_IMP_BTRUE_L	$\btrue \limp P \;\;\defi\;\; P$		A
*	SIMP_SPECIAL_IMP_BFALSE_R	$P \limp \bfalse \;\;\defi\;\; \lnot\, P$		A
*	SIMP_SPECIAL_IMP_BFALSE_L	$\bfalse \limp P \;\;\defi\;\; \btrue$		A
*	SIMP_MULTI_IMP	$P \limp P \;\;\defi\;\; \btrue$		A
*	SIMP_MULTI_IMP_NOT_L	$\lnot P\limp P\;\;\defi\;\; P$		A
*	SIMP_MULTI_IMP_NOT_R	$P\limp\lnot P\;\;\defi\;\;\lnot P$		A
*	SIMP_MULTI_IMP_AND	$P \land \ldots \land Q \land \ldots \land R \limp Q \;\;\defi\;\; \btrue$		A
*	SIMP_MULTI_IMP_AND_NOT_R	$P \land \ldots \land Q \land \ldots \land R \limp \lnot\, Q \;\;\defi\;\; \lnot\,(P \land \ldots \land Q \land \ldots \land R)$		A
*	SIMP_MULTI_IMP_AND_NOT_L	$P \land \ldots \land \lnot\, Q \land \ldots \land R \limp Q \;\;\defi\;\; \lnot\,(P \land \ldots \land \lnot\, Q \land \ldots \land R)$		A
*	SIMP_MULTI_EQV	$P \leqv P \;\;\defi\;\; \btrue$		A
*	SIMP_MULTI_EQV_NOT	$P \leqv \lnot\, P \;\;\defi\;\; \bfalse$		A
*	SIMP_SPECIAL_NOT_BTRUE	$\lnot\, \btrue \;\;\defi\;\; \bfalse$		A
*	SIMP_SPECIAL_NOT_BFALSE	$\lnot\, \bfalse \;\;\defi\;\; \btrue$		A
*	SIMP_NOT_NOT	$\lnot\, \lnot\, P \;\;\defi\;\; P$		AM
*	SIMP_NOTEQUAL	$E \neq F \;\;\defi\;\; \lnot\, E = F$		A
*	SIMP_NOTIN	$E \notin F \;\;\defi\;\; \lnot\, E \in F$		A
*	SIMP_NOTSUBSET	$E \not\subset F \;\;\defi\;\; \lnot\, E \subset F$		A
*	SIMP_NOTSUBSETEQ	$E \not\subseteq F \;\;\defi\;\; \lnot\, E \subseteq F$		A
*	SIMP_NOT_LE	$\lnot\, a \leq b \;\;\defi\;\; a > b$		A
*	SIMP_NOT_GE	$\lnot\, a \geq b \;\;\defi\;\; a < b$		A
*	SIMP_NOT_LT	$\lnot\, a < b \;\;\defi\;\; a \geq b$		A
*	SIMP_NOT_GT	$\lnot\, a > b \;\;\defi\;\; a \leq b$		A
*	SIMP_SPECIAL_NOT_EQUAL_FALSE_R	$\lnot\, (E = \False ) \;\;\defi\;\; (E = \True )$		A
*	SIMP_SPECIAL_NOT_EQUAL_FALSE_L	$\lnot\, (\False = E) \;\;\defi\;\; (\True = E)$		A
*	SIMP_SPECIAL_NOT_EQUAL_TRUE_R	$\lnot\, (E = \True ) \;\;\defi\;\; (E = \False )$		A
*	SIMP_SPECIAL_NOT_EQUAL_TRUE_L	$\lnot\, (\True = E) \;\;\defi\;\; (\False = E)$		A
*	SIMP_FORALL_AND	$\forall x \qdot P \land Q \;\;\defi\;\; (\forall x \qdot P) \land (\forall x \qdot Q)$		A
*	SIMP_EXISTS_OR	$\exists x \qdot P \lor Q \;\;\defi\;\; (\exists x \qdot P) \lor (\exists x \qdot Q)$		A
*	SIMP_EXISTS_IMP	$\exists x\qdot P\limp Q\;\;\defi\;\;(\forall x\qdot P)\limp(\exists x\qdot Q)$		A
*	SIMP_FORALL	$\forall \ldots ,z,\ldots \qdot P(z) \;\;\defi\;\; \forall z \qdot P(z)$	Quantified identifiers other than $z$ do not occur in $P$	A
*	SIMP_EXISTS	$\exists \ldots ,z,\ldots \qdot P(z) \;\;\defi\;\; \exists z \qdot P(z)$	Quantified identifiers other than $z$ do not occur in $P$	A
*	SIMP_MULTI_EQUAL	$E = E \;\;\defi\;\; \btrue$		A
*	SIMP_MULTI_NOTEQUAL	$E \neq E \;\;\defi\;\; \bfalse$		A
*	SIMP_EQUAL_MAPSTO	$E \mapsto F = G \mapsto H \;\;\defi\;\; E = G \land F = H$		A
*	SIMP_EQUAL_SING	$\{ E\} = \{ F\} \;\;\defi\;\; E = F$		A
*	SIMP_SPECIAL_EQUAL_TRUE	$\True = \False \;\;\defi\;\; \bfalse$		A
*	SIMP_TYPE_SUBSETEQ	$S \subseteq \mathit{Ty} \;\;\defi\;\; \btrue$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_SUBSETEQ_SING	$\{ E\} \subseteq S \;\;\defi\;\; E \in S$	where $E$ is a single expression	A
*	SIMP_SPECIAL_SUBSETEQ	$\emptyset \subseteq S \;\;\defi\;\; \btrue$		A
*	SIMP_MULTI_SUBSETEQ	$S \subseteq S \;\;\defi\;\; \btrue$		A
*	SIMP_SUBSETEQ_BUNION	$S \subseteq A \bunion \ldots \bunion S \bunion \ldots \bunion B \;\;\defi\;\; \btrue$		A
*	SIMP_SUBSETEQ_BINTER	$A \binter \ldots \binter S \binter \ldots \binter B \subseteq S \;\;\defi\;\; \btrue$		A
*	DERIV_SUBSETEQ_BUNION	$A \bunion \ldots \bunion B \subseteq S \;\;\defi\;\; A \subseteq S \land \ldots \land B \subseteq S$		A
*	DERIV_SUBSETEQ_BINTER	$S \subseteq A \binter \ldots \binter B \;\;\defi\;\; S \subseteq A \land \ldots \land S \subseteq B$		A
*	SIMP_SPECIAL_IN	$E \in \emptyset \;\;\defi\;\; \bfalse$		A
*	SIMP_MULTI_IN	$B \in \{ A, \ldots , B, \ldots , C\} \;\;\defi\;\; \btrue$		A
*	SIMP_IN_SING	$E \in \{ F\} \;\;\defi\;\; E = F$		A
*	SIMP_MULTI_SETENUM	$\{ A, \ldots , B, \ldots , B, \ldots , C\} \;\;\defi\;\; \{ A, \ldots , B, \ldots , C\}$		A
*	SIMP_SPECIAL_BINTER	$S \binter \ldots \binter \emptyset \binter \ldots \binter T \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_BINTER	$S \binter \ldots \binter \mathit{Ty} \binter \ldots \binter T \;\;\defi\;\; S \binter \ldots \binter T$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_BINTER	$S \binter \ldots \binter T \binter \ldots \binter T \binter \ldots \binter U \;\;\defi\;\; S \binter \ldots \binter T \binter \ldots \binter U$		A
*	SIMP_MULTI_EQUAL_BINTER	$S \binter \ldots \binter T \binter \ldots \binter U = T \;\;\defi\;\; T \subseteq S \binter \ldots \binter U$		A
*	SIMP_SPECIAL_BUNION	$S \bunion \ldots \bunion \emptyset \bunion \ldots \bunion T \;\;\defi\;\; S \bunion \ldots \bunion T$		A
*	SIMP_TYPE_BUNION	$S \bunion \ldots \bunion \mathit{Ty} \bunion \ldots \bunion T \;\;\defi\;\; \mathit{Ty}$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_BUNION	$S \bunion \ldots \bunion T \bunion \ldots \bunion T \bunion \ldots \bunion U \;\;\defi\;\; S \bunion \ldots \bunion T \bunion \ldots \bunion U$		A
*	SIMP_MULTI_EQUAL_BUNION	$S \bunion \ldots \bunion T \bunion \ldots \bunion U = T \;\;\defi\;\; S \bunion \ldots \bunion U \subseteq T$		A
*	SIMP_MULTI_SETMINUS	$S \setminus S \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_SETMINUS_R	$S \setminus \emptyset \;\;\defi\;\; S$		A
*	SIMP_SPECIAL_SETMINUS_L	$\emptyset \setminus S \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_SETMINUS	$S \setminus \mathit{Ty} \;\;\defi\;\; \emptyset$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_TYPE_SETMINUS_SETMINUS	$\mathit{Ty} \setminus (\mathit{Ty} \setminus S) \;\;\defi\;\; S$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_KUNION_POW	$\union (\pow (S)) \;\;\defi\;\; S$		A
*	SIMP_KUNION_POW1	$\union (\pown (S)) \;\;\defi\;\; S$		A
*	SIMP_SPECIAL_KUNION	$\union (\{ \emptyset \} ) \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_QUNION	$\Union x\qdot \bfalse \mid E \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_KINTER	$\inter (\{ \emptyset \} ) \;\;\defi\;\; \emptyset$		A
*	SIMP_KINTER_POW	$\inter (\pow (S)) \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_POW	$\pow (\emptyset ) \;\;\defi\;\; \{ \emptyset \}$		A
*	SIMP_SPECIAL_POW1	$\pown (\emptyset ) \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_CPROD_R	$S \cprod \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_CPROD_L	$\emptyset \cprod S \;\;\defi\;\; \emptyset$		A
	SIMP_COMPSET_EQUAL	$\{ x, y \qdot x = E(y) \land P(y) \mid F(x, y) \} \;\;\defi\;\; \{ y \qdot P(y) \mid F(E(y), y) \}$	where $x$ non free in $E$ and non free in $P$	A
*	SIMP_COMPSET_IN	$\{ x \qdot x \in S \mid x \} \;\;\defi\;\; S$	where $x$ non free in $S$	A
*	SIMP_COMPSET_SUBSETEQ	$\{ x \qdot x \subseteq S \mid x \} \;\;\defi\;\; \pow (S)$	where $x$ non free in $S$	A
*	SIMP_SPECIAL_COMPSET_BFALSE	$\{ x \qdot \bfalse \mid x \} \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_COMPSET_BTRUE	$\{ x \qdot \btrue \mid E \} \;\;\defi\;\; \mathit{Ty}$	where the type of $E$ is $\mathit{Ty}$ and $E$ is a maplet combination of locally-bound, pairwise-distinct bound identifiers	A
*	SIMP_SUBSETEQ_COMPSET_L	$\{ x \qdot P(x) \mid E(x) \} \subseteq S \;\;\defi\;\; \forall y\qdot P(y) \limp E(y) \in S$	where $y$ is fresh	A
*	SIMP_IN_COMPSET	$F \in \{ x,y,\ldots \qdot P(x,y,\ldots) \mid E(x,y,\ldots) \} \;\;\defi\;\; \exists x,y,\ldots \qdot P(x,y,\ldots) \land E(x,y,\ldots) = F$	where $x$ , $y$ , $\ldots$ are not free in $F$	A
*	SIMP_IN_COMPSET_ONEPOINT	$E \in \{ x \qdot P(x) \mid x \} \;\;\defi\;\; P(E)$	Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate	A
	SIMP_SUBSETEQ_COMPSET_R	$S \subseteq \{ x \qdot P(x) \mid x \} \;\;\defi\;\; \forall y\qdot y \in S \limp P(y)$	where $y$ non free in $S, \{ x \qdot P(x) \mid x \}$	M
*	SIMP_SPECIAL_OVERL	$r \ovl \ldots \ovl \emptyset \ovl \ldots \ovl s \;\;\defi\;\; r \ovl \ldots \ovl s$		A
*	SIMP_SPECIAL_KBOOL_BTRUE	$\bool (\btrue ) \;\;\defi\;\; \True$		A
*	SIMP_SPECIAL_KBOOL_BFALSE	$\bool (\bfalse ) \;\;\defi\;\; \False$		A
	DISTRI_SUBSETEQ_BUNION_SING	$S \bunion \{ F\} \subseteq T \;\;\defi\;\; S \subseteq T \land F \in T$	where $F$ is a single expression	M
*	DEF_FINITE	$\finite(S) \;\;\defi\;\; \exists n,f\qdot f\in 1\upto n \tbij S$		M
*	SIMP_SPECIAL_FINITE	$\finite (\emptyset ) \;\;\defi\;\; \btrue$		A
*	SIMP_FINITE_SETENUM	$\finite (\{ a, \ldots , b\} ) \;\;\defi\;\; \btrue$		A
*	SIMP_FINITE_BUNION	$\finite (S \bunion T) \;\;\defi\;\; \finite (S) \land \finite (T)$		A
*	SIMP_FINITE_POW	$\finite (\pow (S)) \;\;\defi\;\; \finite (S)$		A
*	DERIV_FINITE_CPROD	$\finite (S \cprod T) \;\;\defi\;\; S = \emptyset \lor T = \emptyset \lor (\finite (S) \land \finite (T))$		A
*	SIMP_FINITE_CONVERSE	$\finite (r^{-1} ) \;\;\defi\;\; \finite (r)$		A
*	SIMP_FINITE_UPTO	$\finite (a \upto b) \;\;\defi\;\; \btrue$		A
*	SIMP_FINITE_ID	$\finite (\id) \;\;\defi\;\; \finite (S)$	where $\id$ has type $\pow(S \cprod S)$	A
*	SIMP_FINITE_ID_DOMRES	$\finite (E \domres \id) \;\;\defi\;\; \finite (E)$		A
*	SIMP_FINITE_PRJ1	$\finite (\prjone) \;\;\defi\;\; \finite (S \cprod T)$	where $\prjone$ has type $\pow(S \cprod T \cprod S)$	A
*	SIMP_FINITE_PRJ2	$\finite (\prjtwo) \;\;\defi\;\; \finite (S \cprod T)$	where $\prjtwo$ has type $\pow(S \cprod T \cprod T)$	A
*	SIMP_FINITE_PRJ1_DOMRES	$\finite (E \domres \prjone) \;\;\defi\;\; \finite (E)$		A
*	SIMP_FINITE_PRJ2_DOMRES	$\finite (E \domres \prjtwo) \;\;\defi\;\; \finite (E)$		A
*	SIMP_FINITE_NATURAL	$\finite (\nat ) \;\;\defi\;\; \bfalse$		A
*	SIMP_FINITE_NATURAL1	$\finite (\natn ) \;\;\defi\;\; \bfalse$		A
*	SIMP_FINITE_INTEGER	$\finite (\intg ) \;\;\defi\;\; \bfalse$		A
*	SIMP_FINITE_BOOL	$\finite (\Bool ) \;\;\defi\;\; \btrue$		A
*	SIMP_FINITE_LAMBDA	$\finite(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \finite(\{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_TYPE_IN	$t \in \mathit{Ty} \;\;\defi\;\; \btrue$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_SPECIAL_EQV_BTRUE	$P \leqv \btrue \;\;\defi\;\; P$		A
*	SIMP_SPECIAL_EQV_BFALSE	$P \leqv \bfalse \;\;\defi\;\; \lnot\, P$		A
*	DEF_SUBSET	$A \subset B \;\;\defi\;\; A \subseteq B \land \lnot A = B$		A
*	SIMP_SPECIAL_SUBSET_R	$S \subset \emptyset \;\;\defi\;\; \bfalse$		A
*	SIMP_SPECIAL_SUBSET_L	$\emptyset\subset S \;\;\defi\;\; \lnot\; S = \emptyset$		A
*	SIMP_TYPE_SUBSET_L	$S \subset \mathit{Ty} \;\;\defi\;\; S \neq \mathit{Ty}$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_SUBSET	$S \subset S \;\;\defi\;\; \bfalse$		A
*	SIMP_EQUAL_CONSTR	$\operatorname{constr} (a_1, \ldots, a_n) = \operatorname{constr} (b_1, \ldots, b_n) \;\;\defi\;\; a_1 = b_1 \land \ldots \land a_n = b_n$	where $\operatorname{constr}$ is a datatype constructor	A
*	SIMP_EQUAL_CONSTR_DIFF	$\operatorname{constr_1} (\ldots) = \operatorname{constr_2} (\ldots) \;\;\defi\;\; \bfalse$	where $\operatorname{constr_1}$ and $\operatorname{constr_2}$ are different datatype constructors	A
*	SIMP_DESTR_CONSTR	$\operatorname{destr} (\operatorname{constr} (a_1, \ldots, a_n)) \;\;\defi\;\; a_i$	where $\operatorname{destr}$ is the datatype destructor for the i-th argument of datatype constructor $\operatorname{constr}$	A
*	DISTRI_AND_OR	$P \land (Q \lor R) \;\;\defi\;\; (P \land Q) \lor (P \land R)$		M
*	DISTRI_OR_AND	$P \lor (Q \land R) \;\;\defi\;\; (P \lor Q) \land (P \lor R)$		M
*	DEF_OR	$P \lor Q \lor \ldots \lor R \;\;\defi\;\; \lnot\, P \limp (Q \lor \ldots \lor R)$		M
*	DERIV_IMP	$P \limp Q \;\;\defi\;\; \lnot\, Q \limp \lnot\, P$		M
*	DERIV_IMP_IMP	$P \limp (Q \limp R) \;\;\defi\;\; P \land Q \limp R$		M
*	DISTRI_IMP_AND	$P \limp (Q \land R) \;\;\defi\;\; (P \limp Q) \land (P \limp R)$		M
*	DISTRI_IMP_OR	$(P \lor Q) \limp R \;\;\defi\;\; (P \limp R) \land (Q \limp R)$		M
*	DEF_EQV	$P \leqv Q \;\;\defi\;\; (P \limp Q) \land (Q \limp P)$		M
*	DISTRI_NOT_AND	$\lnot\,(P \land Q) \;\;\defi\;\; \lnot\, P \lor \lnot\, Q$		M
*	DISTRI_NOT_OR	$\lnot\,(P \lor Q) \;\;\defi\;\; \lnot\, P \land \lnot\, Q$		M
*	DERIV_NOT_IMP	$\lnot\,(P \limp Q) \;\;\defi\;\; P \land \lnot\, Q$		M
*	DERIV_NOT_FORALL	$\lnot\, \forall x \qdot P \;\;\defi\;\; \exists x \qdot \lnot\, P$		M
*	DERIV_NOT_EXISTS	$\lnot\, \exists x \qdot P \;\;\defi\;\; \forall x \qdot \lnot\, P$		M
*	DEF_IN_MAPSTO	$E \mapsto F \in S \cprod T \;\;\defi\;\; E \in S \land F \in T$		AM
*	DEF_IN_POW	$E \in \pow (S) \;\;\defi\;\; E \subseteq S$		M
*	DEF_IN_POW1	$E \in \pown (S) \;\;\defi\;\; E \in \pow (S) \land S \neq \emptyset$		M
*	DEF_SUBSETEQ	$S \subseteq T \;\;\defi\;\; \forall x \qdot x \in S \limp x \in T$	where $x$ is not free in $S$ or $T$	M
*	DEF_IN_BUNION	$E \in S \bunion T \;\;\defi\;\; E \in S \lor E \in T$		M
*	DEF_IN_BINTER	$E \in S \binter T \;\;\defi\;\; E \in S \land E \in T$		M
*	DEF_IN_SETMINUS	$E \in S \setminus T \;\;\defi\;\; E \in S \land \lnot\,(E \in T)$		M
*	DEF_IN_SETENUM	$E \in \{ A, \ldots , B\} \;\;\defi\;\; E = A \lor \ldots \lor E = B$		M
*	DEF_IN_KUNION	$E \in \union (S) \;\;\defi\;\; \exists s \qdot s \in S \land E \in s$	where $s$ is fresh	M
*	DEF_IN_QUNION	$E \in (\Union x \qdot P(x) \mid T(x)) \;\;\defi\;\; \exists s \qdot P(s) \land E \in T(s)$	where $s$ is fresh	M
*	DEF_IN_KINTER	$E \in \inter (S) \;\;\defi\;\; \forall s \qdot s \in S \limp E \in s$	where $s$ is fresh	M
*	DEF_IN_QINTER	$E \in (\Inter x \qdot P(x) \mid T(x)) \;\;\defi\;\; \forall s \qdot P(s) \limp E \in T(s)$	where $s$ is fresh	M
*	DEF_IN_UPTO	$E \in a \upto b \;\;\defi\;\; a \leq E \land E \leq b$		M
*	DISTRI_BUNION_BINTER	$S \bunion (T \binter U) \;\;\defi\;\; (S \bunion T) \binter (S \bunion U)$		M
*	DISTRI_BINTER_BUNION	$S \binter (T \bunion U) \;\;\defi\;\; (S \binter T) \bunion (S \binter U)$		M
	DISTRI_BINTER_SETMINUS	$S \binter (T \setminus U) \;\;\defi\;\; (S \binter T) \setminus (S \binter U)$		M
	DISTRI_SETMINUS_BUNION	$S \setminus (T \bunion U) \;\;\defi\;\; S \setminus T \setminus U$		M
*	DERIV_TYPE_SETMINUS_BINTER	$\mathit{Ty} \setminus (S \binter T) \;\;\defi\;\; (\mathit{Ty} \setminus S) \bunion (\mathit{Ty} \setminus T)$	where $\mathit{Ty}$ is a type expression	M
*	DERIV_TYPE_SETMINUS_BUNION	$\mathit{Ty} \setminus (S \bunion T) \;\;\defi\;\; (\mathit{Ty} \setminus S) \binter (\mathit{Ty} \setminus T)$	where $\mathit{Ty}$ is a type expression	M
*	DERIV_TYPE_SETMINUS_SETMINUS	$\mathit{Ty} \setminus (S \setminus T) \;\;\defi\;\; (\mathit{Ty} \setminus S) \bunion T$	where $\mathit{Ty}$ is a type expression	M
	DISTRI_CPROD_BINTER	$S \cprod (T \binter U) \;\;\defi\;\; (S \cprod T) \binter (S \cprod U)$		M
	DISTRI_CPROD_BUNION	$S \cprod (T \bunion U) \;\;\defi\;\; (S \cprod T) \bunion (S \cprod U)$		M
	DISTRI_CPROD_SETMINUS	$S \cprod (T \setminus U) \;\;\defi\;\; (S \cprod T) \setminus (S \cprod U)$		M
*	DERIV_SUBSETEQ	$S \subseteq T \;\;\defi\;\; (\mathit{Ty} \setminus T) \subseteq (\mathit{Ty} \setminus S)$	where $\pow (\mathit{Ty})$ is the type of $S$ and $T$	M
*	DERIV_EQUAL	$S = T \;\;\defi\;\; S \subseteq T \land T \subseteq S$	where $\pow (\mathit{Ty})$ is the type of $S$ and $T$	M
*	DERIV_SUBSETEQ_SETMINUS_L	$A \setminus B \subseteq S \;\;\defi\;\; A \subseteq B \bunion S$		M
*	DERIV_SUBSETEQ_SETMINUS_R	$S \subseteq A \setminus B \;\;\defi\;\; S \subseteq A \land S \binter B = \emptyset$		M
*	DEF_PARTITION	$\operatorname{partition} (s, s_1, s_2, \ldots, s_n) \;\;\defi\;\; \begin{array}{ll} & s = s_1\bunion s_2\bunion\cdots\bunion s_n\\ \land& s_1\binter s_2 = \emptyset\\ \vdots\\ \land& s_1\binter s_n = \emptyset\\ \vdots\\ \land& s_{n-1}\binter s_n = \emptyset \end{array}$		AM
*	SIMP_EMPTY_PARTITION	$\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset$		A
*	SIMP_SINGLE_PARTITION	$\operatorname{partition}(S, T) \;\;\defi\;\; S = T$		A
*	DEF_EQUAL_CARD	$\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S$	also works for $k = \operatorname{card}(S)$	M
*	SIMP_EQUAL_CARD	$\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T$		M

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_DOM_SETENUM	$\dom (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ x, \ldots , y\}$		A
*	SIMP_DOM_CONVERSE	$\dom (r^{-1} ) \;\;\defi\;\; \ran (r)$		A
*	SIMP_RAN_SETENUM	$\ran (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ a, \ldots , b\}$		A
*	SIMP_RAN_CONVERSE	$\ran (r^{-1} ) \;\;\defi\;\; \dom (r)$		A
*	SIMP_SPECIAL_OVERL	$r \ovl \ldots \ovl \emptyset \ovl \ldots \ovl s \;\;\defi\;\; r \ovl \ldots \ovl s$		A
*	SIMP_MULTI_OVERL	$r_1 \ovl \cdots \ovl r_n \defi r_1 \ovl \cdots \ovl r_{i-1} \ovl r_{i+1} \ovl \cdots \ovl r_n$	there is a $j$ such that $1\leq i < j \leq n$ and $r_i$ and $r_j$ are syntactically equal.	A
*	SIMP_TYPE_OVERL_CPROD	$r\ovl\cdots\ovl\mathit{Ty}\ovl\cdots\ovl s \;\defi\;\; \mathit{Ty}\ovl\cdots\ovl s$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_SPECIAL_DOMRES_L	$\emptyset \domres r \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_DOMRES_R	$S \domres \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_DOMRES	$\mathit{Ty} \domres r \;\;\defi\;\; r$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_DOMRES_DOM	$\dom (r) \domres r \;\;\defi\;\; r$		A
*	SIMP_MULTI_DOMRES_RAN	$\ran (r) \domres r^{-1} \;\;\defi\;\; r^{-1}$		A
*	SIMP_DOMRES_DOMRES_ID	$S \domres (T \domres \id) \;\;\defi\;\; (S \binter T) \domres \id$		A
*	SIMP_DOMRES_DOMSUB_ID	$S \domres (T \domsub \id) \;\;\defi\;\; (S \setminus T) \domres \id$		A
*	SIMP_SPECIAL_RANRES_R	$r \ranres \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_RANRES_L	$\emptyset \ranres S \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_RANRES	$r \ranres \mathit{Ty} \;\;\defi\;\; r$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_RANRES_RAN	$r \ranres \ran (r) \;\;\defi\;\; r$		A
*	SIMP_MULTI_RANRES_DOM	$r^{-1} \ranres \dom (r) \;\;\defi\;\; r^{-1}$		A
*	SIMP_RANRES_ID	$\id \ranres S \;\;\defi\;\; S \domres \id$		A
*	SIMP_RANSUB_ID	$\id \ransub S \;\;\defi\;\; S \domsub \id$		A
*	SIMP_RANRES_DOMRES_ID	$(S \domres \id) \ranres T \;\;\defi\;\; (S \binter T) \domres \id$		A
*	SIMP_RANRES_DOMSUB_ID	$(S \domsub \id) \ranres T \;\;\defi\;\; (T \setminus S) \domres \id$		A
*	SIMP_SPECIAL_DOMSUB_L	$\emptyset \domsub r \;\;\defi\;\; r$		A
*	SIMP_SPECIAL_DOMSUB_R	$S \domsub \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_DOMSUB	$\mathit{Ty} \domsub r \;\;\defi\;\; \emptyset$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_DOMSUB_DOM	$\dom (r) \domsub r \;\;\defi\;\; \emptyset$		A
*	SIMP_MULTI_DOMSUB_RAN	$\ran (r) \domsub r^{-1} \;\;\defi\;\; \emptyset$		A
*	SIMP_DOMSUB_DOMRES_ID	$S \domsub (T \domres \id ) \;\;\defi\;\; (T \setminus S) \domres \id$		A
*	SIMP_DOMSUB_DOMSUB_ID	$S \domsub (T \domsub \id ) \;\;\defi\;\; (S \bunion T) \domsub \id$		A
*	SIMP_SPECIAL_RANSUB_R	$r \ransub \emptyset \;\;\defi\;\; r$		A
*	SIMP_SPECIAL_RANSUB_L	$\emptyset \ransub S \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_RANSUB	$r \ransub \mathit{Ty} \;\;\defi\;\; \emptyset$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_RANSUB_DOM	$r^{-1} \ransub \dom (r) \;\;\defi\;\; \emptyset$		A
*	SIMP_MULTI_RANSUB_RAN	$r \ransub \ran (r) \;\;\defi\;\; \emptyset$		A
*	SIMP_RANSUB_DOMRES_ID	$(S \domres \id) \ransub T \;\;\defi\;\; (S \setminus T) \domres \id$		A
*	SIMP_RANSUB_DOMSUB_ID	$(S \domsub \id) \ransub T \;\;\defi\;\; (S \bunion T) \domsub \id$		A
*	SIMP_SPECIAL_FCOMP	$r \fcomp \ldots \fcomp \emptyset \fcomp \ldots \fcomp s \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_FCOMP_ID	$r \fcomp \ldots \fcomp \id \fcomp \ldots \fcomp s \;\;\defi\;\; r \fcomp \ldots \fcomp s$		A
*	SIMP_TYPE_FCOMP_R	$r \fcomp \mathit{Ty} \;\;\defi\;\; \dom (r) \cprod \mathit{Tb}$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_TYPE_FCOMP_L	$\mathit{Ty} \fcomp r \;\;\defi\;\; \mathit{Ta} \cprod \ran (r)$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_FCOMP_ID	$r \fcomp \ldots \fcomp S \domres \id \fcomp T \domres \id \fcomp \ldots s \;\;\defi\;\; r \fcomp \ldots \fcomp (S \binter T) \domres \id \fcomp \ldots \fcomp s$		A
*	SIMP_SPECIAL_BCOMP	$r \bcomp \ldots \bcomp \emptyset \bcomp \ldots \bcomp s \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_BCOMP_ID	$r \bcomp \ldots \bcomp \id \bcomp \ldots \bcomp s \;\;\defi\;\; r \bcomp \ldots \bcomp s$		A
*	SIMP_TYPE_BCOMP_L	$\mathit{Ty} \bcomp r \;\;\defi\;\; \dom (r) \cprod \mathit{Tb}$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_TYPE_BCOMP_R	$r \bcomp \mathit{Ty} \;\;\defi\;\; \mathit{Ta} \cprod \ran (r)$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_BCOMP_ID	$r \bcomp \ldots \bcomp S \domres \id \bcomp T \domres \id \bcomp \ldots \bcomp s \;\;\defi\;\; r \bcomp \ldots \bcomp (S \binter T) \domres \id \bcomp \ldots \bcomp s$		A
*	SIMP_SPECIAL_DPROD_R	$r \dprod \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_DPROD_L	$\emptyset \dprod r \;\;\defi\;\; \emptyset$		A
*	SIMP_DPROD_CPROD	$(\mathit{S} \cprod \mathit{T}) \dprod (\mathit{U} \cprod \mathit{V}) \;\;\defi\;\; \mathit{S} \binter \mathit{U} \cprod (\mathit{T} \cprod \mathit{V})$		A
*	SIMP_SPECIAL_PPROD_R	$r \pprod \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_PPROD_L	$\emptyset \pprod r \;\;\defi\;\; \emptyset$		A
*	SIMP_PPROD_CPROD	$(\mathit{S} \cprod \mathit{T}) \pprod (\mathit{U} \cprod \mathit{V}) \;\;\defi\;\; (\mathit{S} \cprod \mathit{U}) \cprod (\mathit{T} \cprod \mathit{V})$		A
*	SIMP_SPECIAL_RELIMAGE_R	$r[\emptyset ] \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_RELIMAGE_L	$\emptyset [S] \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_RELIMAGE	$r[Ty] \;\;\defi\;\; \ran (r)$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_RELIMAGE_DOM	$r[\dom (r)] \;\;\defi\;\; \ran (r)$		A
*	SIMP_RELIMAGE_ID	$\id[T] \;\;\defi\;\; T$		A
*	SIMP_RELIMAGE_DOMRES_ID	$(S \domres \id)[T] \;\;\defi\;\; S \binter T$		A
*	SIMP_RELIMAGE_DOMSUB_ID	$(S \domsub \id)[T] \;\;\defi\;\; T \setminus S$		A
*	SIMP_MULTI_RELIMAGE_CPROD_SING	$(\{ E\} \cprod S)[\{ E\} ] \;\;\defi\;\; S$	where $E$ is a single expression	A
*	SIMP_MULTI_RELIMAGE_SING_MAPSTO	$\{ E \mapsto F\} [\{ E\} ] \;\;\defi\;\; \{ F\}$	where $E$ is a single expression	A
*	SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB	$(r \ransub S)^{-1} [S] \;\;\defi\;\; \emptyset$		A
*	SIMP_MULTI_RELIMAGE_CONVERSE_RANRES	$(r \ranres S)^{-1} [S] \;\;\defi\;\; r^{-1} [S]$		A
*	SIMP_RELIMAGE_CONVERSE_DOMSUB	$(S \domsub r)^{-1} [T] \;\;\defi\;\; r^{-1} [T] \setminus S$		A
	DERIV_RELIMAGE_RANSUB	$(r \ransub S)[T] \;\;\defi\;\; r[T] \setminus S$		M
	DERIV_RELIMAGE_RANRES	$(r \ranres S)[T] \;\;\defi\;\; r[T] \binter S$		M
*	SIMP_MULTI_RELIMAGE_DOMSUB	$(S \domsub r)[S] \;\;\defi\;\; \emptyset$		A
	DERIV_RELIMAGE_DOMSUB	$(S \domsub r)[T] \;\;\defi\;\; r[T \setminus S]$		M
	DERIV_RELIMAGE_DOMRES	$(S \domres r)[T] \;\;\defi\;\; r[S \binter T]$		M
*	SIMP_SPECIAL_CONVERSE	$\emptyset ^{-1} \;\;\defi\;\; \emptyset$		A
*	SIMP_CONVERSE_ID	$\id^{-1} \;\;\defi\;\; \id$		A
*	SIMP_CONVERSE_CPROD	$(\mathit{S} \cprod \mathit{T})^{-1} \;\;\defi\;\; \mathit{T} \cprod \mathit{S}$		A
*	SIMP_CONVERSE_SETENUM	$\{ x \mapsto a, \ldots , y \mapsto b\} ^{-1} \;\;\defi\;\; \{ a \mapsto x, \ldots , b \mapsto y\}$		A
*	SIMP_CONVERSE_COMPSET	$\{ X \qdot P \mid x\mapsto y\} ^{-1} \;\;\defi\;\; \{ X \qdot P \mid y\mapsto x\}$		A
*	SIMP_DOM_ID	$\dom (\id) \;\;\defi\;\; S$	where $\id$ has type $\pow(S \cprod S)$	A
*	SIMP_RAN_ID	$\ran (\id) \;\;\defi\;\; S$	where $\id$ has type $\pow(S \cprod S)$	A
*	SIMP_FCOMP_ID_L	$(S \domres \id) \fcomp r \;\;\defi\;\; S \domres r$		A
*	SIMP_FCOMP_ID_R	$r \fcomp (S \domres \id) \;\;\defi\;\; r \ranres S$		A
*	SIMP_SPECIAL_REL_R	$S \rel \emptyset \;\;\defi\;\; \{ \emptyset \}$	idem for operators $\srel \pfun \pinj \psur$	A
*	SIMP_SPECIAL_REL_L	$\emptyset \rel S \;\;\defi\;\; \{ \emptyset \}$	idem for operators $\trel \pfun \tfun \pinj \tinj$	A
*	SIMP_FUNIMAGE_PRJ1	$\prjone (E \mapsto F) \;\;\defi\;\; E$		A
*	SIMP_FUNIMAGE_PRJ2	$\prjtwo (E \mapsto F) \;\;\defi\;\; F$		A
*	SIMP_DOM_PRJ1	$\dom (\prjone) \;\;\defi\;\; S \cprod T$	where $\prjone$ has type $\pow(S \cprod T \cprod S)$	A
*	SIMP_DOM_PRJ2	$\dom (\prjtwo) \;\;\defi\;\; S \cprod T$	where $\prjtwo$ has type $\pow(S \cprod T \cprod T)$	A
*	SIMP_RAN_PRJ1	$\ran (\prjone) \;\;\defi\;\; S$	where $\prjone$ has type $\pow(S \cprod T \cprod S)$	A
*	SIMP_RAN_PRJ2	$\ran (\prjtwo) \;\;\defi\;\; T$	where $\prjtwo$ has type $\pow(S \cprod T \cprod T)$	A
*	SIMP_FUNIMAGE_LAMBDA	$(\lambda x \qdot P(x) \mid E(x))(y) \;\;\defi\;\; E(y)$		A
*	SIMP_DOM_LAMBDA	$\dom(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid E\}$		A
*	SIMP_RAN_LAMBDA	$\ran(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid F\}$		A
*	SIMP_IN_FUNIMAGE	$E\mapsto F(E)\in F \;\;\defi\;\; \btrue$		A
*	SIMP_IN_FUNIMAGE_CONVERSE_L	$F^{-1}(E)\mapsto E\in F \;\;\defi\;\; \btrue$		A
*	SIMP_IN_FUNIMAGE_CONVERSE_R	$F(E)\mapsto E\in F^{-1} \;\;\defi\;\; \btrue$		A
*	SIMP_MULTI_FUNIMAGE_SETENUM_LL	$\{ A \mapsto E, \ldots , B \mapsto E\} (x) \;\;\defi\;\; E$		A
*	SIMP_MULTI_FUNIMAGE_SETENUM_LR	$\{ E, \ldots , x \mapsto y, \ldots , F\} (x) \;\;\defi\;\; y$		A
*	SIMP_MULTI_FUNIMAGE_OVERL_SETENUM	$(r \ovl \ldots \ovl \{ E, \ldots , x \mapsto y, \ldots , F\} )(x) \;\;\defi\;\; y$		A
*	SIMP_MULTI_FUNIMAGE_BUNION_SETENUM	$(r \bunion \ldots \bunion \{ E, \ldots , x \mapsto y, \ldots , F\} )(x) \;\;\defi\;\; y$		A
*	SIMP_FUNIMAGE_CPROD	$(S \cprod \{ F\} )(x) \;\;\defi\;\; F$		A
*	SIMP_FUNIMAGE_ID	$\id (x) \;\;\defi\;\; x$		A
*	SIMP_FUNIMAGE_FUNIMAGE_CONVERSE	$f(f^{-1} (E)) \;\;\defi\;\; E$		A
*	SIMP_FUNIMAGE_CONVERSE_FUNIMAGE	$f^{-1}(f(E)) \;\;\defi\;\; E$		A
*	SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM	$\{x \mapsto a, \ldots, y \mapsto b\}(\{a \mapsto x, \ldots, b \mapsto y\}(E)) \;\;\defi\;\; E$		A
*	SIMP_FUNIMAGE_DOMRES	$(E \domres F)(G)\;\;\defi\;\;F(G)$	with hypothesis $F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$ , $\tfun$ , $\pinj$ , $\tinj$ , $\psur$ , $\tsur$ , $\tbij$ .	AM
*	SIMP_FUNIMAGE_DOMSUB	$(E \domsub F)(G)\;\;\defi\;\;F(G)$	with hypothesis $F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$ , $\tfun$ , $\pinj$ , $\tinj$ , $\psur$ , $\tsur$ , $\tbij$ .	AM
*	SIMP_FUNIMAGE_RANRES	$(F\ranres E)(G)\;\;\defi\;\;F(G)$	with hypothesis $F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$ , $\tfun$ , $\pinj$ , $\tinj$ , $\psur$ , $\tsur$ , $\tbij$ .	AM
*	SIMP_FUNIMAGE_RANSUB	$(F \ransub E)(G)\;\;\defi\;\;F(G)$	with hypothesis $F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$ , $\tfun$ , $\pinj$ , $\tinj$ , $\psur$ , $\tsur$ , $\tbij$ .	AM
*	SIMP_FUNIMAGE_SETMINUS	$(F \setminus E)(G)\;\;\defi\;\;F(G)$	with hypothesis $F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$ , $\tfun$ , $\pinj$ , $\tinj$ , $\psur$ , $\tsur$ , $\tbij$ .	AM
	DEF_EQUAL_FUNIMAGE	$f(x) = y \;\;\defi\;\; x \mapsto y \in f$		M
*	DEF_BCOMP	$r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r$		M
	DERIV_ID_SING	$\{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\}$	where $E$ is a single expression	M
*	SIMP_SPECIAL_DOM	$\dom (\emptyset ) \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_RAN	$\ran (\emptyset ) \;\;\defi\;\; \emptyset$		A
*	SIMP_CONVERSE_CONVERSE	$r^{-1-1} \;\;\defi\;\; r$		A
*	DERIV_RELIMAGE_FCOMP	$(p \fcomp q)[s] \;\;\defi\;\; q[p[s]]$		M
*	DERIV_FCOMP_DOMRES	$(s \domres p) \fcomp q \;\;\defi\;\; s \domres (p \fcomp q)$		M
*	DERIV_FCOMP_DOMSUB	$(s \domsub p) \fcomp q \;\;\defi\;\; s \domsub (p \fcomp q)$		M
*	DERIV_FCOMP_RANRES	$p \fcomp (q \ranres s) \;\;\defi\;\; (p \fcomp q) \ranres s$		M
*	DERIV_FCOMP_RANSUB	$p \fcomp (q \ransub s) \;\;\defi\;\; (p \fcomp q) \ransub s$		M
	DERIV_FCOMP_SING	$\{E\mapsto F\}\fcomp\{F\mapsto G\} \;\;\defi\;\; \{E\mapsto G\}$		A
*	SIMP_SPECIAL_EQUAL_RELDOMRAN	$\emptyset \strel \emptyset \;\;\defi\;\; \{ \emptyset \}$	idem for operators $\tsur \tbij$	A
*	SIMP_TYPE_DOM	$\dom (\mathit{Ty}) \;\;\defi\;\; \mathit{Ta}$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_TYPE_RAN	$\ran (\mathit{Ty}) \;\;\defi\;\; \mathit{Tb}$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_MULTI_DOM_CPROD	$\dom (E \cprod E) \;\;\defi\;\; E$		A
*	SIMP_MULTI_RAN_CPROD	$\ran (E \cprod E) \;\;\defi\;\; E$		A
*	SIMP_MULTI_DOM_DOMRES	$\dom(A\domres f) \;\;\defi\;\; \dom(f)\binter A$		A
*	SIMP_MULTI_DOM_DOMSUB	$\dom(A\domsub f) \;\;\defi\;\; \dom(f)\setminus A$		A
*	SIMP_MULTI_RAN_RANRES	$\ran(f\ranres A) \;\;\defi\;\; \ran(f)\binter A$		A
*	SIMP_MULTI_RAN_RANSUB	$\ran(f\ransub A) \;\;\defi\;\; \ran(f)\setminus A$		A
*	DEF_IN_DOM	$E \in \dom (r) \;\;\defi\;\; \exists y \qdot E \mapsto y \in r$		M
*	DEF_IN_RAN	$F \in \ran (r) \;\;\defi\;\; \exists x \qdot x \mapsto F \in r$		M
*	DEF_IN_CONVERSE	$E \mapsto F \in r^{-1} \;\;\defi\;\; F \mapsto E \in r$		M
*	DEF_IN_DOMRES	$E \mapsto F \in S \domres r \;\;\defi\;\; E \in S \land E \mapsto F \in r$		M
*	DEF_IN_RANRES	$E \mapsto F \in r \ranres T \;\;\defi\;\; E \mapsto F \in r \land F \in T$		M
*	DEF_IN_DOMSUB	$E \mapsto F \in S \domsub r \;\;\defi\;\; E \notin S \land E \mapsto F \in r$		M
*	DEF_IN_RANSUB	$E \mapsto F \in r \ranres T \;\;\defi\;\; E \mapsto F \in r \land F \notin T$		M
*	DEF_IN_RELIMAGE	$F \in r[w] \;\;\defi\;\; \exists x \qdot x \in w \land x \mapsto F \in r$		M
*	DEF_IN_FCOMP	$E \mapsto F \in (p \fcomp q) \;\;\defi\;\; \exists x \qdot E \mapsto x \in p \land x \mapsto F \in q$		M
*	DEF_OVERL	$p \ovl q \;\;\defi\;\; (\dom (q) \domsub p) \bunion q$		M
*	DEF_IN_ID	$E \mapsto F \in \id \;\;\defi\;\; E = F$		M
*	DEF_IN_DPROD	$E \mapsto (F \mapsto G) \in p \dprod q \;\;\defi\;\; E \mapsto F \in p \land E \mapsto G \in q$		M
*	DEF_IN_PPROD	$(E \mapsto G) \mapsto (F \mapsto H) \in p \pprod q \;\;\defi\;\; E \mapsto F \in p \land G \mapsto H \in q$		M
*	DEF_IN_REL	$r \in S \rel T \;\;\defi\;\; r\subseteq S\cprod T$		M
*	DEF_IN_RELDOM	$r \in S \trel T \;\;\defi\;\; r \in S \rel T \land \dom (r) = S$		M
*	DEF_IN_RELRAN	$r \in S \srel T \;\;\defi\;\; r \in S \rel T \land \ran (r) = T$		M
*	DEF_IN_RELDOMRAN	$r \in S \strel T \;\;\defi\;\; r \in S \rel T \land \dom (r) = S \land \ran (r) = T$		M
*	DEF_IN_FCT	$\begin{array}{rcl} f \in S \pfun T & \defi & f \in S \rel T \\ & \land & (\forall x,y,z \qdot x \mapsto y \in f \land x \mapsto z \in f \limp y = z) \\ \end{array}$		M
*	DEF_IN_TFCT	$f \in S \tfun T \;\;\defi\;\; f \in S \pfun T \land \dom (f) = S$		M
*	DEF_IN_INJ	$f \in S \pinj T \;\;\defi\;\; f \in S \pfun T \land f^{-1} \in T \pfun S$		M
*	DEF_IN_TINJ	$f \in S \tinj T \;\;\defi\;\; f \in S \pinj T \land \dom (f) = S$		M
*	DEF_IN_SURJ	$f \in S \psur T \;\;\defi\;\; f \in S \pfun T \land \ran (f) = T$		M
*	DEF_IN_TSURJ	$f \in S \tsur T \;\;\defi\;\; f \in S \psur T \land \dom (f) = S$		M
*	DEF_IN_BIJ	$f \in S \tbij T \;\;\defi\;\; f \in S \tinj T \land \ran (f) = T$		M
	DISTRI_BCOMP_BUNION	$r \bcomp (s \bunion t) \;\;\defi\;\; (r \bcomp s) \bunion (r \bcomp t)$		M
*	DISTRI_FCOMP_BUNION_R	$p \fcomp (q \bunion r) \;\;\defi\;\; (p \fcomp q) \bunion (p \fcomp r)$		M
*	DISTRI_FCOMP_BUNION_L	$(q \bunion r) \fcomp p \;\;\defi\;\; (q \fcomp p) \bunion (r \fcomp p)$		M
	DISTRI_DPROD_BUNION	$r \dprod (s \bunion t) \;\;\defi\;\; (r \dprod s) \bunion (r \dprod t)$		M
	DISTRI_DPROD_BINTER	$r \dprod (s \binter t) \;\;\defi\;\; (r \dprod s) \binter (r \dprod t)$		M
	DISTRI_DPROD_SETMINUS	$r \dprod (s \setminus t) \;\;\defi\;\; (r \dprod s) \setminus (r \dprod t)$		M
	DISTRI_DPROD_OVERL	$r \dprod (s \ovl t) \;\;\defi\;\; (r \dprod s) \ovl (r \dprod t)$		M
	DISTRI_PPROD_BUNION	$r \pprod (s \bunion t) \;\;\defi\;\; (r \pprod s) \bunion (r \pprod t)$		M
	DISTRI_PPROD_BINTER	$r \pprod (s \binter t) \;\;\defi\;\; (r \pprod s) \binter (r \pprod t)$		M
	DISTRI_PPROD_SETMINUS	$r \pprod (s \setminus t) \;\;\defi\;\; (r \pprod s) \setminus (r \pprod t)$		M
	DISTRI_PPROD_OVERL	$r \pprod (s \ovl t) \;\;\defi\;\; (r \pprod s) \ovl (r \pprod t)$		M
	DISTRI_OVERL_BUNION_L	$(p \bunion q) \ovl r \;\;\defi\;\; (p \ovl r) \bunion (q \ovl r)$		M
	DISTRI_OVERL_BINTER_L	$(p \binter q) \ovl r \;\;\defi\;\; (p \ovl r) \binter (q \ovl r)$		M
*	DISTRI_DOMRES_BUNION_R	$s \domres (p \bunion q) \;\;\defi\;\; (s \domres p) \bunion (s \domres q)$		M
*	DISTRI_DOMRES_BUNION_L	$(s \bunion t) \domres r \;\;\defi\;\; (s \domres r) \bunion (t \domres r)$		M
*	DISTRI_DOMRES_BINTER_R	$s \domres (p \binter q) \;\;\defi\;\; (s \domres p) \binter (s \domres q)$		M
*	DISTRI_DOMRES_BINTER_L	$(s \binter t) \domres r \;\;\defi\;\; (s \domres r) \binter (t \domres r)$		M
	DISTRI_DOMRES_SETMINUS_R	$s \domres (p \setminus q) \;\;\defi\;\; (s \domres p) \setminus (s \domres q)$		M
	DISTRI_DOMRES_SETMINUS_L	$(s \setminus t) \domres r \;\;\defi\;\; (s \domres r) \setminus (t \domres r)$		M
	DISTRI_DOMRES_DPROD	$s \domres (p \dprod q) \;\;\defi\;\; (s \domres p) \dprod (s \domres q)$		M
	DISTRI_DOMRES_OVERL	$s \domres (r \ovl q) \;\;\defi\;\; (s \domres r) \ovl (s \domres q)$		M
*	DISTRI_DOMSUB_BUNION_R	$s \domsub (p \bunion q) \;\;\defi\;\; (s \domsub p) \bunion (s \domsub q)$		M
*	DISTRI_DOMSUB_BUNION_L	$(s \bunion t) \domsub r \;\;\defi\;\; (s \domsub r) \binter (t \domsub r)$		M
*	DISTRI_DOMSUB_BINTER_R	$s \domsub (p \binter q) \;\;\defi\;\; (s \domsub p) \binter (s \domsub q)$		M
*	DISTRI_DOMSUB_BINTER_L	$(s \binter t) \domsub r \;\;\defi\;\; (s \domsub r) \bunion (t \domsub r)$		M
	DISTRI_DOMSUB_DPROD	$A \domsub (r \dprod s) \;\;\defi\;\; (A \domsub r) \dprod (A \domsub s)$		M
	DISTRI_DOMSUB_OVERL	$A \domsub (r \ovl s) \;\;\defi\;\; (A \domsub r) \ovl (A \domsub s)$		M
*	DISTRI_RANRES_BUNION_R	$r \ranres (s \bunion t) \;\;\defi\;\; (r \ranres s) \bunion (r \ranres t)$		M
*	DISTRI_RANRES_BUNION_L	$(p \bunion q) \ranres s \;\;\defi\;\; (p \ranres s) \bunion (q \ranres s)$		M
*	DISTRI_RANRES_BINTER_R	$r \ranres (s \binter t) \;\;\defi\;\; (r \ranres s) \binter (r \ranres t)$		M
*	DISTRI_RANRES_BINTER_L	$(p \binter q) \ranres s \;\;\defi\;\; (p \ranres s) \binter (q \ranres s)$		M
	DISTRI_RANRES_SETMINUS_R	$r \ranres (s \setminus t) \;\;\defi\;\; (r \ranres s) \setminus (r \ranres t)$		M
	DISTRI_RANRES_SETMINUS_L	$(p \setminus q) \ranres s \;\;\defi\;\; (p \ranres s) \setminus (q \ranres s)$		M
*	DISTRI_RANSUB_BUNION_R	$r \ransub (s\bunion t) \;\;\defi\;\; (r \ransub s) \binter (r \ransub t)$		M
*	DISTRI_RANSUB_BUNION_L	$(p \bunion q) \ransub s \;\;\defi\;\; (p \ransub s) \bunion (q \ransub s)$		M
*	DISTRI_RANSUB_BINTER_R	$r \ransub (s \binter t) \;\;\defi\;\; (r \ransub s) \bunion (r \ransub t)$		M
*	DISTRI_RANSUB_BINTER_L	$(p \binter q) \ransub s \;\;\defi\;\; (p \ransub s) \binter (q \ransub s)$		M
*	DISTRI_CONVERSE_BUNION	$(p \bunion q)^{-1} \;\;\defi\;\; p^{-1} \bunion q^{-1}$		M
	DISTRI_CONVERSE_BINTER	$(p \binter q)^{-1} \;\;\defi\;\; p^{-1} \binter q^{-1}$		M
	DISTRI_CONVERSE_SETMINUS	$(r \setminus s)^{-1} \;\;\defi\;\; r^{-1} \setminus s^{-1}$		M
	DISTRI_CONVERSE_BCOMP	$(r \bcomp s)^{-1} \;\;\defi\;\; (s^{-1} \bcomp r^{-1} )$		M
	DISTRI_CONVERSE_FCOMP	$(p \fcomp q)^{-1} \;\;\defi\;\; (q^{-1} \fcomp p^{-1} )$		M
	DISTRI_CONVERSE_PPROD	$(r \pprod s)^{-1} \;\;\defi\;\; r^{-1} \pprod s^{-1}$		M
	DISTRI_CONVERSE_DOMRES	$(s \domres r)^{-1} \;\;\defi\;\; r^{-1} \ranres s$		M
	DISTRI_CONVERSE_DOMSUB	$(s \domsub r)^{-1} \;\;\defi\;\; r^{-1} \ransub s$		M
	DISTRI_CONVERSE_RANRES	$(r \ranres s)^{-1} \;\;\defi\;\; s \domres r^{-1}$		M
	DISTRI_CONVERSE_RANSUB	$(r \ransub s)^{-1} \;\;\defi\;\; s \domsub r^{-1}$		M
*	DISTRI_DOM_BUNION	$\dom (r \bunion s) \;\;\defi\;\; \dom (r) \bunion \dom (s)$		M
*	DISTRI_RAN_BUNION	$\ran (r \bunion s) \;\;\defi\;\; \ran (r) \bunion \ran (s)$		M
*	DISTRI_RELIMAGE_BUNION_R	$r[S \bunion T] \;\;\defi\;\; r[S] \bunion r[T]$		M
*	DISTRI_RELIMAGE_BUNION_L	$(p \bunion q)[S] \;\;\defi\;\; p[S] \bunion q[S]$		M
*	DERIV_DOM_TOTALREL	$\dom (r) \;\;\defi\;\; E$	with hypothesis $r \in E \ \mathit{op}\ F$ , where $\mathit{op}$ is one of $\trel, \strel, \tfun, \tinj, \tsur, \tbij$	M
	DERIV_RAN_SURJREL	$\ran (r) \;\;\defi\;\; F$	with hypothesis $r \in E \ \mathit{op}\ F$ , where $\mathit{op}$ is one of $\srel,\strel, \psur, \tsur, \tbij$	M
*	DERIV_PRJ1_SURJ	$\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue$	where $\mathit{Ty}_1$ and $\mathit{Ty}_2$ are types and $\mathit{op}$ is one of $\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur$	A
*	DERIV_PRJ2_SURJ	$\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue$	where $\mathit{Ty}_1$ and $\mathit{Ty}_2$ are types and $\mathit{op}$ is one of $\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur$	A
*	DERIV_ID_BIJ	$\id \in\mathit{Ty}\ \mathit{op}\ \mathit{Ty}\;\;\defi\;\; \btrue$	where $\mathit{Ty}$ is a type and $\mathit{op}$ is any arrow	A
*	SIMP_MAPSTO_PRJ1_PRJ2	$\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E$		A
	DERIV_EXPAND_PRJS	$E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E)$		M
*	SIMP_DOM_SUCC	$\dom(\usucc) \;\;\defi\;\; \intg$		A
*	SIMP_RAN_SUCC	$\ran(\usucc) \;\;\defi\;\; \intg$		A
*	DERIV_MULTI_IN_BUNION	$E\in A\bunion\cdots\bunion\left\{\cdots, E,\cdots\right\}\bunion\cdots\bunion B\;\;\defi\;\; \btrue$		A
*	DERIV_MULTI_IN_SETMINUS	$E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse$		A
*	DEF_PRED	$\upred\;\;\defi\;\; \usucc^{-1}$		A
	SIMP_SPECIAL_IN_ID	$E \mapsto E \in \id \;\;\defi\;\; \btrue$		A
	SIMP_SPECIAL_IN_SETMINUS_ID	$E \mapsto E \in r \setminus \id \;\;\defi\;\; \bfalse$		A
	SIMP_SPECIAL_IN_DOMRES_ID	$E \mapsto E \in S \domres \id \;\;\defi\;\; E \in S$		A
	SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID	$E \mapsto E \in r \setminus (S \domres \id) \;\;\defi\;\; E \mapsto E \in S \domsub r$		A

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_MIN_IN	$\min (S) \in S \;\;\defi\;\; \btrue$		A
	SIMP_MAX_IN	$\max (S) \in S \;\;\defi\;\; \btrue$		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
	SIMP_KBOOL_LIT_EQUAL_TRUE	$\bool (B = \True) \;\;\defi\;\; B$		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
	DEF_EXPN_STEP	$E ^ P \;\;\defi\;\; E * E ^{(P - 1)}$	with an additional PO $\lnot\, P = 0$	M
*	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

Difference between pages "Adding Reasoners(How to extend Rodin Tutorial)" and "All Rewrite Rules"

Revision as of 16:15, 11 February 2009

Navigation menu

Page actions

Page actions

Personal tools

Navigation

contribute

Search

Tools

@@ Line 1: / Line 1: @@
-{{Navigation|Previous= [[Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) | Generating the proof obligations]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]]}}
+This page groups together all the rewrite rules implemented (or planned for implementation) in the Rodin prover. The rules themselves can be found in the following locations (for editing purposes):
+* [[Set Rewrite Rules]]
+* [[Relation Rewrite Rules]]
+* [[Arithmetic Rewrite Rules]]
-=== Principles ===
+Conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_rules]]
-Rodin support several provers. Some are embedded such as NewPP, or the sequent prover which will talk about here, and some are added by external plug-ins (as the Atelier B provers : ML, PP, P0, etc).
-Contributing to Rodin sequent prover is done by adding tactics. These tactics which often involve a set of reasoners, apply on proof tree nodes. The reasoners apply on the sequent of a given proof tree node. A reasoner is (and has to be) quite "rough" : it shall take a given sequent and produce a proof rule that will (if possible) apply on this given sequent, whereas a tactic could be smarter. Indeed, a tactic can involve several reasoners, thus apply them in loops, and combine them, or even call other tactics. A tactic can be either automatic (auto tactic and/or post tactic) or manual (using providers in the UI that paint their applications in red on formulas) in case of interactive proof.<br>
+{{:Set Rewrite Rules}}
-[[Image:Adding_Reasoners_TacticsImage.png|400px|center]]
+{{:Relation Rewrite Rules}}
-A reasoner encapsulates a kind of "proof step", also called "proof rule". The sequent prover provides a set of tactics applying proof rules (and even other tactics!). These rules are either rewriting rules (see [[All_Rewrite_Rules|rewriting rule list]]) or inference rules (see [[Inference_Rules|inference rule list]]). It is actually a really critical piece of code, that developers should understand at first sight, and be convinced about its correctness. If one codes a wrong reasoner, one breaks the whole soundness of proofs done within Rodin! As they are written in pure java, and accorded to the previous considerations, they have to be the simpliest and most readable as possible. Finally, it is needed to write tests that cover all the possible cases of application of one given reasoner (this will not be detailed in this tutorial).
+{{:Arithmetic Rewrite Rules}}
-=== In this part ===
-In this part we will see how to contribute to the sequent prover of Rodin by encapsulating a new proof rule within a reasoner and add a tactic to the sequent prover of Rodin that will encapsulate this reasoner.
-The rule, coded within the reasoner, that we want to apply is the following:
-{| cellpadding="20" cellspacing="0" border="1"
-|<math>\frac{ \textbf{H},\; a = b \;\; \vdash \;\; \textbf{G}} {\textbf{H},\; a \leq b,\;b \leq a\;\vdash \;\; \textbf{G}}</math>
-| DBL_INEQ
-|}
-Let's call this rule DBL_INEQ. By reading this rule, we see it is goal agnostic. This means that the rule will be applied if the prover sequent under consideration contains the hypotheses <math>a \leq b,\;b \leq a</math>, whatever the goal of this sequent. We will say that <math>a \leq b,\;b \leq a</math> are the "Needed hypotheses".
-[[Image:Adding_Reasoners_DBL_INEQ_Reasoner.png|550px|center]]
-Moreover, <math>\textbf{H}</math> is the set of selected hypotheses from the input sequent, and <math> a \leq b,\;b \leq a\;\vdash \;\textbf{G}</math> is the antecedent of the rule (i.e. a child node to be proved).
-=== Step1 ===
-* Create a new plugin that will host our reasoner and tactic. It will not be any activator for this plug-in but the option "Activate this plug-in when one of its classes is loaded" shall be selected.
-* Add a dependencies to the plug-ins <tt>org.eclipse.core.resources</tt>, <tt>org.eclipse.core.runtime</tt>, <tt>org.eclipse.ui</tt>, <tt>org.rodinp.core</tt>, <tt>org.eventb.core.ast</tt>,<tt>org.eventb.core.seqprover</tt> and <tt>org.eventb.core</tt>.
-* Add the extension point <tt>org.eventb.core.seaqprover.reasoners</tt>, and create a 'reasoner' extension for our reasoner with ''"id : dblIneq"'' and ''"name :  Double Inequality"'' and finally,
-* Create a new class for the reasoner, called <tt>DoubleInequalityReasoner</tt>.
-=== Step2 ===
-Implement the body of the reasoner :
-* the reasoner shall "<tt>implements IVersionedReasoner</tt>" thus <tt>getVersion()</tt> shall return a static integer giving the current version of our reasoner. 0 might not be a wrong choice for our first try. <tt>getReasonerID()</tt> shall return a unique ID. It MUST correspond to the id given in the reasoner extension we created, and is prefixed by the plugin id where it lays. Here, we didn't create any activator for our plugin, so no such constant prefix exists. So, let's create here something like :
- private static final String REASONER_ID = "org.eventb.doubleInequality.dblIneq";
-You should now have something close to this :
- public class DoubleInequalityReasoner implements IVersionedReasoner {
- 	private static final int VERSION = 0;
- 	private static final String REASONER_ID = "org.eventb.doubleInequality.dblIneq";
- 	@Override
- 	public String getReasonerID() {
- 		return REASONER_ID;
- 	}
- 	@Override
- 	public int getVersion() {
- 		return VERSION;
- 	}
- 	@Override
- 	public IReasonerOutput apply(IProverSequent seq, IReasonerInput input,
- 			IProofMonitor pm) {
-        }
-=== Step3 / Exercise ===
-Implement the method public <tt>IReasonerOutput '''apply'''(IProverSequent seq, IReasonerInput input, IProofMonitor pm)</tt>. This method is the place where one shall create the proof rule to be applied from the input sequent <tt>seq</tt> and with the given input if needed.
-Here is the list of tasks you have to perform in this <tt>apply()</tt> method :
-* get and check the input predicate a <= b,
-* check the presence of the other hypothesis b <= a,
-* make the new hypothesis a=b that will be in the antecedent produced by our rule,
-* make the antecedent (see the picture above) where a <= b and b <= a are deselected(i.e. hidden) so that the tactic does not apply in unfinite loop,
-* make the proof rule to return,
-=== Step4 ===
-Here we see together the solution proposed for the implementation of the <tt>apply()</tt> method of our reasoner:
- @Override
- public IReasonerOutput apply(IProverSequent seq, IReasonerInput input, IProofMonitor pm) {
-* get and check the input predicate a <= b
-NB : Here we suppose that the given input doesn't have any error. If it has, we shall return a <tt>reasonerFailure</tt>(See <tt>ProverFactory.reasonerFailure()</tt> method for more details).<br>
-We want our <tt>IReasonerInput</tt> to be a predicate input of the form "a <= b". Thus, there is an existing class to reuse : <tt>SinglePredInput</tt>.<br>
-Please, have a look at <tt>IReasonerInput</tt> implementation hierarchy to see which kind of input classes exist and that you could reuse in your reasoners.<br>
-[[Image:IReasonerInput.png|400px|center]]
-Thus, here is what you should write :
-   if (input.hasError()) {
-     return ProverFactory.reasonerFailure(this, input, input.getError());
-   }
-   final SinglePredInput predInput = (SinglePredInput) input;
-   final Predicate predicate = predInput.getPredicate();
-   if (predicate.getTag() != Formula.LE) {
-     return ProverFactory.reasonerFailure(this, input, "invalid input predicate");
-   }
-* check the presence of the other hypothesis b <= a
-   // we are sure that the predicate is a relational predicate as we checked that getTag() == Formula.LE
-   final RelationalPredicate aLEb = (RelationalPredicate) predicate;
-   final Expression a = aLEb.getLeft();
-   final Expression b = aLEb.getRight();
-   final FormulaFactory ff = seq.getFormulaFactory(); // we retrieve the formula factory
-   final Predicate bLEa = ff.makeRelationalPredicate(Formula.LE, b, a,	null); // we build b <= a
-   if (!seq.containsHypotheses(Arrays.asList(aLEb, bLEa))) {
-     return ProverFactory.reasonerFailure(this, input,"sequent does not contain required hypotheses");
-   }
-* make the new hypothesis a=b
-NB : we reuse the formula factory that we got from the sequent to create the new hypothesis <tt>a = b</tt> :
-   final Predicate aEqb = ff.makeRelationalPredicate(Formula.EQUAL, a, b, null);
-* make the antecedent
-   // we create the added hypothesis a = b
-   final Set<Predicate> addedHyps = Collections.singleton(aEqb);
-   // we hide a <= b and b <= a
-   final ISelectionHypAction hideIneqs = ProverFactory.makeHideHypAction(Arrays.asList(aLEb, bLEa));
-   // we create our antecedent to be used in our proof rule
-   final IAntecedent antecedent = ProverFactory.makeAntecedent(null, addedHyps, hideIneqs);
-* make the proof rule to return
-   // We do not forget to say that a <= b (aLEb) and b <= a (bLEa) are needed for our rule to be applied
-   final Set<Predicate> neededHyps = new HashSet<Predicate>();
-   neededHyps.addAll(Arrays.asList(aLEb, bLEa));
-   // We return the proof rule corresponding to DBL_INEQ
-   return ProverFactory.makeProofRule(this, input, null, neededHyps, "Inequality Rewrites", antecedent);
-  }
-=== Step5 ===
-As our input is actually a SinglePredInput, which as its name describes, holds a predicate, our reasoner is actually a specialisation of the abstract class SinglePredInputReasoner.
-Please check the other proposed (e.g. published) types of reasoners corresponding to existing inputs among :
-* SingleExprInputReasoner,
-* SinglePredInputReasoner,
-* SingleStringInputReasoner,
-* EmptyInputReasoner,
-* ForwardInfReasoner,
-* HypothesisReasoner,
-* XProverInputReasoner.
-In our case, simply add the <tt>extends SinglePredInputReasoner</tt> to the declaration of the reasoner class.
-And this is all for our reasoner! Now let's add a tactic corresponding to it.
-=== Step6 ===
-Now that we have the reasoner DoubleInequalityReasoner, we need to create a tactic to call this reasoner when possible.
-We want this reasoner, for more convenience, to be applied automatically. Thus we define an auto-tactic that will call our reasoner.
-* Add the extension point <tt>org.eventb.core.seqprover.autoTactics</tt> to our plugin,
-* create an extension ''autoTactic'' for a new tactic we will create here with :
-:- ''id : dblIneqTac'',<br>
-:- ''name : Double Inequality Tactic'',<br>
-:- ''description : Applies Double Inequality Rule'',<br>
-:- ''auto : place the boolean to <tt>true</tt> to let the tactic be automatic'',<br>
-:- ''post : place the boolean to <tt>true</tt> so the tactic will no execute as a post tactic'',<br>
-:- And now it remains the tactic ''class'' to create. So, create the tactic class <tt>DoubleInequalityTactic</tt> which <tt>implements ITactic</tt>.<br>
-In this tactic, what we have to do is to calculate if the current proof tree node contains an application of the reasoner, and if it is the case, call the reasoner.
-You can see that the only method to implement is : <tt>apply(IProofTreeNode ptNode, IProofMonitor pm)</tt>
-We will detail here, what one should do in this method:
- @Override
- public Object apply(IProofTreeNode ptNode, IProofMonitor pm) {
-* First, we search for double inequalities ''a <= b'' and ''b <= a'' in the selected hypotheses. To search it, we traverse all the selected hypotheses via <tt>sequent.selectedHypIterable()</tt>.
- final IProverSequent sequent = ptNode.getSequent();
- final FormulaFactory ff = sequent.getFormulaFactory();
-   for (Predicate hyp : sequent.selectedHypIterable()) {
-* Then, when we encounter one hypothesis of the form E <= F (e.g. hypothesis.getTag() == Formula.LE), then we build the hypothesis F <= E :
- 	if (hyp.getTag() == Formula.LE) {
- 		final RelationalPredicate aLEb = (RelationalPredicate) hyp;
- 		final Expression a = aLEb.getLeft();
- 		final Expression b = aLEb.getRight();
- 		final RelationalPredicate bLEa = ff.makeRelationalPredicate(Formula.LE, b, a, null);
-* if the sequent contains this latter hypothesis, we call the reasoner DoubleInequalityReasoner (encapsulated in a tactic)
- 		if(sequent.containsHypothesis(bLEa)) {
-                 	return callDblIneqReasoner(ptNode, aLEb, pm);
-  		}
- 	}
-  }
-  return "no double inequality hypotheses found";
- }
-As we need to construct the SinglePredInput with the hypothesis a <= b, and then apply our reasoner, the usual way to do this, is to encapsulate this reasoner call into a tactic. There is a facility to do that offered by <tt>BasicTactics.reasonerTac</tt>. Thus we write the following :
-  private Object callDblIneqReasoner(IProofTreeNode ptNode, final RelationalPredicate inputPred, IProofMonitor pm) {
-   final ITactic dblIneqTac = BasicTactics.reasonerTac(new DoubleInequalityReasoner(), new SinglePredInput(inputPred));
-   return dblIneqTac.apply(ptNode, pm);
-  }
-where at line 2 we encapsulate the reasoner call, and at line 3, we apply the reasoner.
-=== Conclusion ===
-That's it for the addition of reasoners in the seqprover.
-Now you can try it by creating a simple context for example, with the two hypotheses as axioms and another theorem such as a = 2.<br>
-By running the auto-provers, you should see that the Inequality Rewrites is applied.
-N.B: if you don't see any application of our reasoner, you might have forgotten to select the corresponding tactic to the auto tactic profile which is applied.
-Go to ''Window > Prefences'', and then in ''Event-B category > Sequent Prover'', select the "Auto/Post Tactic" preferences and create a new profile and add the ''Double Inequality Tactic'' to it.<br />
-You can select it from the list on the left within the profile editor (see the picture below):
-[[Image:DBL_INEQ_Preferences.png|650px]]
-{{Navigation|Previous= [[Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) | Generating the proof obligations]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]]}}
-[[Category:Developer documentation|*Index]]
-[[Category:Rodin Platform|*Index]]
-[[Category:Tutorial|*Index]]