All Rewrite Rules

From Event-B
Revision as of 13:29, 26 April 2013 by imported>Laurent (Add Empty Set Rewrite Rules)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search
CAUTION! Any modification to this page shall be announced on the User mailing list!

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

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

Set 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

Relation 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_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

Empty Set 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.

All rewrite rules that match the pattern \textbf{P}=\emptyset are also applicable to predicates of the form \textbf{P}\subseteq\emptyset and \emptyset=\textbf{P}, as these predicates are equivalent. All rewrite rules that match the pattern \textbf{P}=\mathit{Ty} are also applicable to predicates of the form \mathit{Ty}\subseteq\textbf{P} and \mathit{Ty}=\textbf{P}, as these predicates are equivalent.


  Name Rule Side Condition A/M
*
DEF_SPECIAL_NOT_EQUAL
  \lnot\, S = \emptyset  \;\;\defi\;\;  \exists x \qdot  x \in  S where x is not free in S M
*
SIMP_SETENUM_EQUAL_EMPTY
  \{ A, \ldots , B\}  = \emptyset \;\;\defi\;\;  \bfalse A
*
SIMP_SPECIAL_EQUAL_COMPSET
  \{  x \qdot  P(x) \mid  E \}  = \emptyset  \;\;\defi\;\;  \forall x\qdot  \lnot\, P(x) A
*
SIMP_BINTER_EQUAL_TYPE
  A \binter \cdots \binter B = \mathit{Ty} \;\;\defi\;\;  A = \mathit{Ty} \land \cdots \land B  = \mathit{Ty} where \mathit{Ty} is a type expression A
*
SIMP_BINTER_SING_EQUAL_EMPTY
A\binter\cdots\binter\{a\}\binter\cdots\binter B  = \emptyset  \;\;\defi\;\;  \lnot\, a \in A\binter\cdots\binter B A
*
SIMP_BINTER_SETMINUS_EQUAL_EMPTY
A\binter\cdots\binter(B\setminus C)\binter\cdots\binter D  = \emptyset  \;\;\defi\;\;  (A\binter\cdots\binter B\binter\cdots\binter D) \setminus C = \emptyset A
*
SIMP_BUNION_EQUAL_EMPTY
  A \bunion \cdots \bunion B = \emptyset \;\;\defi\;\;  A = \emptyset \land \cdots \land B  = \emptyset A
*
SIMP_SETMINUS_EQUAL_EMPTY
  A \setminus  B = \emptyset \;\;\defi\;\;  A \subseteq  B  A
*
SIMP_SETMINUS_EQUAL_TYPE
  A \setminus  B = \mathit{Ty} \;\;\defi\;\;  A = \mathit{Ty} \land B = \emptyset where \mathit{Ty} is a type expression A
*
SIMP_POW_EQUAL_EMPTY
  \pow (S) = \emptyset \;\;\defi\;\;  \bfalse  A
*
SIMP_POW1_EQUAL_EMPTY
  \pown (S) = \emptyset \;\;\defi\;\;  S = \emptyset  A
*
SIMP_KINTER_EQUAL_TYPE
   \inter (S) = \mathit{Ty} \;\;\defi\;\;  S = \{ \mathit{Ty} \}  where \mathit{Ty} is a type expression A
*
SIMP_KUNION_EQUAL_EMPTY
   \union (S) = \emptyset \;\;\defi\;\;  S \subseteq \{ \emptyset \}  A
*
SIMP_QINTER_EQUAL_TYPE
  (\Inter  x\qdot P(x)  \mid  E(x)) = \mathit{Ty} \;\;\defi\;\;  \forall x\qdot  P(x) \limp E(x) = \mathit{Ty} where \mathit{Ty} is a type expression A
*
SIMP_QUNION_EQUAL_EMPTY
  (\Union  x\qdot P(x)  \mid  E(x)) = \emptyset \;\;\defi\;\;  \forall x\qdot  P(x) \limp E(x) = \emptyset A
*
SIMP_NATURAL_EQUAL_EMPTY
  \nat = \emptyset \;\;\defi\;\;  \bfalse A
*
SIMP_NATURAL1_EQUAL_EMPTY
  \natn = \emptyset \;\;\defi\;\;  \bfalse A
*
SIMP_TYPE_EQUAL_EMPTY
 \mathit{Ty} = \emptyset  \;\;\defi\;\;  \bfalse where \mathit{Ty} is a type expression A
*
SIMP_CPROD_EQUAL_EMPTY
  S \cprod T = \emptyset \;\;\defi\;\; S = \emptyset \lor T = \emptyset A
*
SIMP_CPROD_EQUAL_TYPE
  S \cprod T = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land T = \mathit{Tb} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
*
SIMP_UPTO_EQUAL_EMPTY
  i \upto j = \emptyset \;\;\defi\;\; i > j A
*
SIMP_UPTO_EQUAL_INTEGER
  i \upto j = \intg \;\;\defi\;\; \bfalse A
*
SIMP_UPTO_EQUAL_NATURAL
  i \upto j = \nat \;\;\defi\;\; \bfalse A
*
SIMP_UPTO_EQUAL_NATURAL1
  i \upto j = \natn \;\;\defi\;\; \bfalse A
*
SIMP_SPECIAL_EQUAL_REL
  A \rel  B = \emptyset  \;\;\defi\;\;  \bfalse idem for operators \pfun  \pinj A
SIMP_TYPE_EQUAL_REL
  A \rel  B = \mathit{Ty}  \;\;\defi\;\;  A = \mathit{Ta} \land B = \mathit{Tb} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
*
SIMP_SPECIAL_EQUAL_RELDOM
  A \trel  B = \emptyset  \;\;\defi\;\;  \lnot\, A = \emptyset  \land  B = \emptyset idem for operator \tfun A
SIMP_TYPE_EQUAL_RELDOMRAN
  A \trel  B = \mathit{Ty}  \;\;\defi\;\;  \bfalse where \mathit{Ty} is a type expression, idem for operator \srel, \strel, \tfun, \tinj, \psur, \tsur, \tbij A
*
SIMP_SREL_EQUAL_EMPTY
  A \srel B = \emptyset \;\;\defi\;\; A = \emptyset \land  \lnot\,B = \emptyset A
*
SIMP_STREL_EQUAL_EMPTY
  A \strel B = \emptyset \;\;\defi\;\; (A = \emptyset \leqv  \lnot\,B = \emptyset) A
*
SIMP_DOM_EQUAL_EMPTY
  \dom (r) = \emptyset \;\;\defi\;\; r = \emptyset  A
*
SIMP_RAN_EQUAL_EMPTY
  \ran (r) = \emptyset \;\;\defi\;\; r = \emptyset  A
*
SIMP_FCOMP_EQUAL_EMPTY
 p \fcomp q = \emptyset \;\;\defi\;\; \ran (p) \binter \dom (q) = \emptyset  A
*
SIMP_BCOMP_EQUAL_EMPTY
 p \bcomp q = \emptyset \;\;\defi\;\; \ran (q) \binter \dom (p) = \emptyset  A
*
SIMP_DOMRES_EQUAL_EMPTY
 S \domres r = \emptyset \;\;\defi\;\; \dom (r) \binter S = \emptyset  A
*
SIMP_DOMRES_EQUAL_TYPE
 S \domres r = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land r = \mathit{Ty}  where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
*
SIMP_DOMSUB_EQUAL_EMPTY
 S \domsub r = \emptyset \;\;\defi\;\; \dom (r) \subseteq S A
*
SIMP_DOMSUB_EQUAL_TYPE
 S \domsub r = \mathit{Ty} \;\;\defi\;\; S = \emptyset \land r = \mathit{Ty} where \mathit{Ty} is a type expression A
*
SIMP_RANRES_EQUAL_EMPTY
 r \ranres S = \emptyset \;\;\defi\;\; \ran (r) \binter S = \emptyset A
*
SIMP_RANRES_EQUAL_TYPE
 r \ranres S = \mathit{Ty} \;\;\defi\;\; S = \mathit{Tb} \land r = \mathit{Ty} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
*
SIMP_RANSUB_EQUAL_EMPTY
 r \ransub S = \emptyset \;\;\defi\;\; \ran (r) \subseteq S A
*
SIMP_RANSUB_EQUAL_TYPE
 r \ransub S = \mathit{Ty} \;\;\defi\;\; S = \emptyset \land r = \mathit{Ty} where \mathit{Ty} is a type expression A
*
SIMP_CONVERSE_EQUAL_EMPTY
 r^{-1} = \emptyset \;\;\defi\;\; r = \emptyset A
*
SIMP_CONVERSE_EQUAL_TYPE
 r^{-1} = \mathit{Ty} \;\;\defi\;\; r = \mathit{Ty}^{-1} where \mathit{Ty} is a type expression A
*
SIMP_RELIMAGE_EQUAL_EMPTY
 r[S] = \emptyset \;\;\defi\;\; S \domres r = \emptyset A
*
SIMP_OVERL_EQUAL_EMPTY
  r \ovl \cdots \ovl s = \emptyset \;\;\defi\;\; r = \emptyset \land \cdots \land s =  \emptyset A
*
SIMP_DPROD_EQUAL_EMPTY
  p \dprod q = \emptyset \;\;\defi\;\; \dom (p) \binter \dom (q) = \emptyset A
*
SIMP_DPROD_EQUAL_TYPE
  p \dprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Ta} \cprod \mathit{Tc} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod (\mathit{Tb} \cprod \mathit{Tc}) A
*
SIMP_PPROD_EQUAL_EMPTY
  p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset A
*
SIMP_PPROD_EQUAL_TYPE
  p \pprod q = \mathit{Ty} \;\;\defi\;\;  p = \mathit{Ta} \cprod \mathit{Tc} \land q = \mathit{Tb} \cprod \mathit{Td} where \mathit{Ty} is a type expression equal to (\mathit{Ta} \cprod \mathit{Tb}) \cprod (\mathit{Tc} \cprod \mathit{Td}) A
*
SIMP_ID_EQUAL_EMPTY
  \id = \emptyset \;\;\defi\;\; \bfalse A
*
SIMP_PRJ1_EQUAL_EMPTY
  \prjone = \emptyset \;\;\defi\;\; \bfalse A
*
SIMP_PRJ2_EQUAL_EMPTY
  \prjtwo = \emptyset \;\;\defi\;\; \bfalse A

Arithmetic 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_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

Extension Proof 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.

Rewrite Rules

  Name Rule Side Condition A/M
*
SIMP_SPECIAL_COND_BTRUE
  \operatorname{COND}(\btrue, E_1, E_2)  \;\;\defi\;\;  E_1 A
*
SIMP_SPECIAL_COND_BFALSE
  \operatorname{COND}(\bfalse, E_1, E_2)  \;\;\defi\;\;  E_2 A
*
SIMP_MULTI_COND
  \operatorname{COND}(C, E, E)  \;\;\defi\;\;  E A

Inference Rules

  Name Rule Side Condition A/M
*
DATATYPE_DISTINCT_CASE
\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H}  \;\;\vdash\;\;  \textbf{G} } where x has a datatype DT as type and appears free in \textbf{G}, DT has constructors c_1, \ldots, c_n, parameters p_{ij} are introduced as fresh identifiers M


*
DATATYPE_INDUCTION
\frac{ \textbf{H}, x=c_1(p_1, \ldots, p_k),\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l})  \;\;\vdash \;\; \textbf{P}(x)  \qquad \ldots \qquad}{ \textbf{H}  \;\;\vdash\;\;  \textbf{P}(x) } where x has inductive datatype DT as type and appears free in \textbf{P}; \{p_{I_1}, \ldots, p_{I_l}\} \subseteq \{p_1, \ldots, p_k\} are the inductive parameters (if any); an antecedent is created for every constructor c_i of DT; all parameters are introduced as fresh identifiers; examples here M