Difference between revisions of "All Rewrite Rules"

From Event-B
Jump to navigationJump to search
imported>Nicolas
m (added section for extension rewrite rules)
imported>Nicolas
m (FIxed link to Extension Proof Rules)
Line 14: Line 14:
 
{{:Arithmetic Rewrite Rules}}
 
{{:Arithmetic Rewrite Rules}}
  
==[[Extension Rewrite Rules]]==
+
==[[Extension Proof Rules]]==
{{:Extension Rewrite Rules}}
+
{{:Extension Proof Rules}}

Revision as of 12:56, 10 September 2010

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

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