Set Rewrite Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Laurent Added side condition to SIMP_IN_COMPSET |
Rules SIMP_{EMPTY,SINGLE}_PARTITION were implemented |
||
(66 intermediate revisions by 8 users not shown) | |||
Line 1: | Line 1: | ||
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin. | |||
Rules without a <tt>*</tt> are planned to be implemented in future versions. | |||
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]]. | |||
{{RRHeader}} | {{RRHeader}} | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_AND_BTRUE}}||<math> P \land \ldots \land \btrue \land \ldots \land Q \;\;\defi\;\; P \land \ldots \land Q </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_AND_BTRUE}}||<math> P \land \ldots \land \btrue \land \ldots \land Q \;\;\defi\;\; P \land \ldots \land Q </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_AND_BFALSE}}||<math> P \land \ldots \land \bfalse \land \ldots \land Q \;\;\defi\;\; \bfalse </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_AND_BFALSE}}||<math> P \land \ldots \land \bfalse \land \ldots \land Q \;\;\defi\;\; \bfalse </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_MULTI_AND}}||<math> P \land \ldots \land Q \land \ldots \land Q \land \ldots \land R \;\;\defi\;\; P \land \ldots \land Q \land \ldots \land R </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_AND}}||<math> P \land \ldots \land Q \land \ldots \land Q \land \ldots \land R \;\;\defi\;\; P \land \ldots \land Q \land \ldots \land R </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_MULTI_AND_NOT}}||<math> P \land \ldots \land Q \land \ldots \land \lnot\, Q \land \ldots \land R \;\;\defi\;\; \bfalse </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_AND_NOT}}||<math> P \land \ldots \land Q \land \ldots \land \lnot\, Q \land \ldots \land R \;\;\defi\;\; \bfalse </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OR_BTRUE}}||<math> P \lor \ldots \lor \btrue \lor \ldots \lor Q \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OR_BTRUE}}||<math> P \lor \ldots \lor \btrue \lor \ldots \lor Q \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OR_BFALSE}}||<math> P \lor \ldots \lor \bfalse \lor \ldots \lor Q \;\;\defi\;\; P \lor \ldots \lor Q </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OR_BFALSE}}||<math> P \lor \ldots \lor \bfalse \lor \ldots \lor Q \;\;\defi\;\; P \lor \ldots \lor Q </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_MULTI_OR}}||<math> P \lor \ldots \lor Q \lor \ldots \lor Q \lor \ldots \lor R \;\;\defi\;\; P \lor \ldots \lor Q \lor \ldots \lor R </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_OR}}||<math> P \lor \ldots \lor Q \lor \ldots \lor Q \lor \ldots \lor R \;\;\defi\;\; P \lor \ldots \lor Q \lor \ldots \lor R </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_MULTI_OR_NOT}}||<math> P \lor \ldots \lor Q \lor \ldots \lor \lnot\, Q \land \ldots \land R \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_OR_NOT}}||<math> P \lor \ldots \lor Q \lor \ldots \lor \lnot\, Q \land \ldots \land R \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BTRUE_R}}||<math> P \limp \btrue \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BTRUE_R}}||<math> P \limp \btrue \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BTRUE_L}}||<math> \btrue \limp P \;\;\defi\;\; P </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BTRUE_L}}||<math> \btrue \limp P \;\;\defi\;\; P </math>|| || A | ||
Line 13: | Line 17: | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BFALSE_L}}||<math> \bfalse \limp P \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BFALSE_L}}||<math> \bfalse \limp P \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP}}||<math> P \limp P \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP}}||<math> P \limp P \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP_NOT_L}}||<math>\lnot P\limp P\;\;\defi\;\; P</math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_MULTI_IMP_AND_NOT_R}}||<math> P \land \ldots \land Q \land \ldots \land R \limp \lnot\, Q \;\;\defi\;\; \lnot\,(P \land \ldots \land Q \land \ldots \land R) </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP_NOT_R}}||<math>P\limp\lnot P\;\;\defi\;\;\lnot P</math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_MULTI_IMP_AND_NOT_L}}||<math> P \land \ldots \land \lnot\, Q \land \ldots \land R \limp Q \;\;\defi\;\; \lnot\,(P \land \ldots \land \lnot\, Q \land \ldots \land R) </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP_AND}}||<math> P \land \ldots \land Q \land \ldots \land R \limp Q \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP_AND_NOT_R}}||<math> P \land \ldots \land Q \land \ldots \land R \limp \lnot\, Q \;\;\defi\;\; \lnot\,(P \land \ldots \land Q \land \ldots \land R) </math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP_AND_NOT_L}}||<math> P \land \ldots \land \lnot\, Q \land \ldots \land R \limp Q \;\;\defi\;\; \lnot\,(P \land \ldots \land \lnot\, Q \land \ldots \land R) </math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQV}}||<math> P \leqv P \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_EQV}}||<math> P \leqv P \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_MULTI_EQV_NOT}}||<math> P \leqv \lnot\, P \;\;\defi\;\; \bfalse | {{RRRow}}|*||{{Rulename|SIMP_MULTI_EQV_NOT}}||<math> P \leqv \lnot\, P \;\;\defi\;\; \bfalse </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_BTRUE}}||<math> \lnot\, \btrue \;\;\defi\;\; \bfalse </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_BTRUE}}||<math> \lnot\, \btrue \;\;\defi\;\; \bfalse </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_BFALSE}}||<math> \lnot\, \bfalse \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_BFALSE}}||<math> \lnot\, \bfalse \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_NOT_NOT}}||<math> \lnot\, \lnot\, P \;\;\defi\;\; P </math>|| || | {{RRRow}}|*||{{Rulename|SIMP_NOT_NOT}}||<math> \lnot\, \lnot\, P \;\;\defi\;\; P </math>|| || AM | ||
{{RRRow}}|*||{{Rulename|SIMP_NOTEQUAL}}||<math> E \neq F \;\;\defi\;\; \lnot\, E = F </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_NOTEQUAL}}||<math> E \neq F \;\;\defi\;\; \lnot\, E = F </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_NOTIN}}||<math> E \notin F \;\;\defi\;\; \lnot\, E \in F </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_NOTIN}}||<math> E \notin F \;\;\defi\;\; \lnot\, E \in F </math>|| || A | ||
Line 36: | Line 41: | ||
{{RRRow}}|*||{{Rulename|SIMP_FORALL_AND}}||<math> \forall x \qdot P \land Q \;\;\defi\;\; (\forall x \qdot P) \land (\forall x \qdot Q) </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_FORALL_AND}}||<math> \forall x \qdot P \land Q \;\;\defi\;\; (\forall x \qdot P) \land (\forall x \qdot Q) </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_EXISTS_OR}}||<math> \exists x \qdot P \lor Q \;\;\defi\;\; (\exists x \qdot P) \lor (\exists x \qdot Q) </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_EXISTS_OR}}||<math> \exists x \qdot P \lor Q \;\;\defi\;\; (\exists x \qdot P) \lor (\exists x \qdot Q) </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_FORALL}}||<math> \forall \ldots ,z,\ldots \qdot P(z) \;\;\defi\;\; \forall z \qdot P(z) </math>|| Quantified identifiers other than <math>z</math> do not occur in <math>P</math> || A | {{RRRow}}|*||{{Rulename|SIMP_EXISTS_IMP}}||<math>\exists x\qdot P\limp Q\;\;\defi\;\;(\forall x\qdot P)\limp(\exists x\qdot Q)</math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_EXISTS}}||<math> \exists \ldots ,z,\ldots \qdot P(z) \;\;\defi\;\; \exists z \qdot P(z) </math>|| Quantified identifiers other than <math>z</math> do not occur in <math>P</math> || A | {{RRRow}}|*||{{Rulename|SIMP_FORALL}}||<math> \forall \ldots ,z,\ldots \qdot P(z) \;\;\defi\;\; \forall z \qdot P(z) </math>|| Quantified identifiers other than <math>z</math> do not occur in <math>P</math> || A | ||
{{RRRow}}|*||{{Rulename|SIMP_EXISTS}}||<math> \exists \ldots ,z,\ldots \qdot P(z) \;\;\defi\;\; \exists z \qdot P(z) </math>|| Quantified identifiers other than <math>z</math> do not occur in <math>P</math> || A | |||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQUAL}}||<math> E = E \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_EQUAL}}||<math> E = E \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_NOTEQUAL}}||<math> E \neq E \;\;\defi\;\; \bfalse </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_NOTEQUAL}}||<math> E \neq E \;\;\defi\;\; \bfalse </math>|| || A | ||
Line 43: | Line 49: | ||
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_SING}}||<math> \{ E\} = \{ F\} \;\;\defi\;\; E = F </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_EQUAL_SING}}||<math> \{ E\} = \{ F\} \;\;\defi\;\; E = F </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_TRUE}}||<math> \True = \False \;\;\defi\;\; \bfalse </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_TRUE}}||<math> \True = \False \;\;\defi\;\; \bfalse </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_TYPE_SUBSETEQ}}||<math> S \subseteq \mathit{Ty} \;\;\defi\;\; \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression || A | {{RRRow}}|*||{{Rulename|SIMP_TYPE_SUBSETEQ}}||<math> S \subseteq \mathit{Ty} \;\;\defi\;\; \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
{{RRRow}}|||{{Rulename|SIMP_SUBSETEQ_SING}}||<math> \{ E\} \subseteq S \;\;\defi\;\; E \in S </math>|| where <math>E</math> is a single expression || A | {{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_SING}}||<math> \{ E\} \subseteq S \;\;\defi\;\; E \in S </math>|| where <math>E</math> is a single expression || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SUBSETEQ}}||<math> \emptyset \subseteq S \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SUBSETEQ}}||<math> \emptyset \subseteq S \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_SUBSETEQ}}||<math> S \subseteq S \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_SUBSETEQ}}||<math> S \subseteq S \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_BUNION}}||<math> S \subseteq A \bunion \ldots \bunion S \bunion \ldots \bunion B \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_BUNION}}||<math> S \subseteq A \bunion \ldots \bunion S \bunion \ldots \bunion B \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_BINTER}}||<math> A \binter \ldots \binter S \binter \ldots \binter B \subseteq S \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_BINTER}}||<math> A \binter \ldots \binter S \binter \ldots \binter B \subseteq S \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ_BUNION}}||<math> A \bunion \ldots \bunion B \subseteq S \;\;\defi\;\; A \subseteq S \land \ldots \land B \subseteq S </math>|| || | {{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ_BUNION}}||<math> A \bunion \ldots \bunion B \subseteq S \;\;\defi\;\; A \subseteq S \land \ldots \land B \subseteq S </math>|| || A | ||
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ_BINTER}}||<math> S \subseteq A \binter \ldots \binter B \;\;\defi\;\; S \subseteq A \land \ldots \land S \subseteq B </math>|| || | {{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ_BINTER}}||<math> S \subseteq A \binter \ldots \binter B \;\;\defi\;\; S \subseteq A \land \ldots \land S \subseteq B </math>|| || A | ||
<!-- | |||
{{RRRow}}|||{{Rulename|SIMP_SUBSET_BUNION}}||<math> A \bunion \ldots \bunion B \subset S \;\;\defi\;\; A \subset S \land \ldots \land B \subset S </math>|| || A | {{RRRow}}|||{{Rulename|SIMP_SUBSET_BUNION}}||<math> A \bunion \ldots \bunion B \subset S \;\;\defi\;\; A \subset S \land \ldots \land B \subset S </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_SUBSET_BINTER}}||<math> S \subset A \binter \ldots \binter B \;\;\defi\;\; S \subset A \land \ldots \land S \subset B </math>|| || A | {{RRRow}}|||{{Rulename|SIMP_SUBSET_BINTER}}||<math> S \subset A \binter \ldots \binter B \;\;\defi\;\; S \subset A \land \ldots \land S \subset B </math>|| || A | ||
--> | |||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN}}||<math> E \in \emptyset \;\;\defi\;\; \bfalse </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN}}||<math> E \in \emptyset \;\;\defi\;\; \bfalse </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IN}}||<math> B \in \{ A, \ldots , B, \ldots , C\} \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_IN}}||<math> B \in \{ A, \ldots , B, \ldots , C\} \;\;\defi\;\; \btrue </math>|| || A | ||
Line 60: | Line 68: | ||
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BINTER}}||<math> S \binter \ldots \binter \mathit{Ty} \binter \ldots \binter T \;\;\defi\;\; S \binter \ldots \binter T </math>|| where <math>\mathit{Ty}</math> is a type expression || A | {{RRRow}}|*||{{Rulename|SIMP_TYPE_BINTER}}||<math> S \binter \ldots \binter \mathit{Ty} \binter \ldots \binter T \;\;\defi\;\; S \binter \ldots \binter T </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_BINTER}}||<math> S \binter \ldots \binter T \binter \ldots \binter T \binter \ldots \binter U \;\;\defi\;\; S \binter \ldots \binter T \binter \ldots \binter U </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_BINTER}}||<math> S \binter \ldots \binter T \binter \ldots \binter T \binter \ldots \binter U \;\;\defi\;\; S \binter \ldots \binter T \binter \ldots \binter U </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_MULTI_EQUAL_BINTER}}||<math> S \binter \ldots \binter T \binter \ldots \binter U = T \;\;\defi\;\; T \subseteq S \binter \ldots \binter U </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_EQUAL_BINTER}}||<math> S \binter \ldots \binter T \binter \ldots \binter U = T \;\;\defi\;\; T \subseteq S \binter \ldots \binter U </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_BUNION}}||<math> S \bunion \ldots \bunion \emptyset \bunion \ldots \bunion T \;\;\defi\;\; S \bunion \ldots \bunion T </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_BUNION}}||<math> S \bunion \ldots \bunion \emptyset \bunion \ldots \bunion T \;\;\defi\;\; S \bunion \ldots \bunion T </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BUNION}}||<math> S \bunion \ldots \bunion \mathit{Ty} \bunion \ldots \bunion T \;\;\defi\;\; \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression || A | {{RRRow}}|*||{{Rulename|SIMP_TYPE_BUNION}}||<math> S \bunion \ldots \bunion \mathit{Ty} \bunion \ldots \bunion T \;\;\defi\;\; \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_BUNION}}||<math> S \bunion \ldots \bunion T \bunion \ldots \bunion T \bunion \ldots \bunion U \;\;\defi\;\; S \bunion \ldots \bunion T \bunion \ldots \bunion U </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_BUNION}}||<math> S \bunion \ldots \bunion T \bunion \ldots \bunion T \bunion \ldots \bunion U \;\;\defi\;\; S \bunion \ldots \bunion T \bunion \ldots \bunion U </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_MULTI_EQUAL_BUNION}}||<math> S \bunion \ldots \bunion T \bunion \ldots \bunion U = T \;\;\defi\;\; S \bunion \ldots \bunion U \subseteq T </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_EQUAL_BUNION}}||<math> S \bunion \ldots \bunion T \bunion \ldots \bunion U = T \;\;\defi\;\; S \bunion \ldots \bunion U \subseteq T </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_SETMINUS}}||<math> S \setminus S \;\;\defi\;\; \emptyset </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_SETMINUS}}||<math> S \setminus S \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SETMINUS_R}}||<math> S \setminus \emptyset \;\;\defi\;\; S </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SETMINUS_R}}||<math> S \setminus \emptyset \;\;\defi\;\; S </math>|| || A | ||
Line 70: | Line 78: | ||
{{RRRow}}|*||{{Rulename|SIMP_TYPE_SETMINUS}}||<math> S \setminus \mathit{Ty} \;\;\defi\;\; \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression || A | {{RRRow}}|*||{{Rulename|SIMP_TYPE_SETMINUS}}||<math> S \setminus \mathit{Ty} \;\;\defi\;\; \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
{{RRRow}}|*||{{Rulename|SIMP_TYPE_SETMINUS_SETMINUS}}||<math> \mathit{Ty} \setminus (\mathit{Ty} \setminus S) \;\;\defi\;\; S </math>|| where <math>\mathit{Ty}</math> is a type expression || A | {{RRRow}}|*||{{Rulename|SIMP_TYPE_SETMINUS_SETMINUS}}||<math> \mathit{Ty} \setminus (\mathit{Ty} \setminus S) \;\;\defi\;\; S </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
{{RRRow}}| | {{RRRow}}|*||{{Rulename|SIMP_KUNION_POW}}||<math> \union (\pow (S)) \;\;\defi\;\; S </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_KUNION_POW1}}||<math> \union (\pown (S)) \;\;\defi\;\; S </math>|| || A | |||
{{RRRow}}|||{{Rulename|SIMP_KUNION_POW1}}||<math> \union (\pown (S)) \;\;\defi\;\; S </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KUNION}}||<math> \union (\{ \emptyset \} ) \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_KUNION}}||<math> \union \{ \emptyset \} ) \;\;\defi\;\; \emptyset </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_QUNION}}||<math> \Union x\qdot \bfalse \mid E \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_QUNION}}||<math> \Union x\qdot \bfalse \mid E \;\;\defi\;\; \emptyset </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KINTER}}||<math> \inter (\{ \emptyset \} ) \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_KINTER}}||<math> \inter (\{ \emptyset \} ) \;\;\defi\;\; \emptyset </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_KINTER_POW}}||<math> \inter (\pow (S)) \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_POW}}||<math> \pow (\emptyset ) \;\;\defi\;\; \{ \emptyset \} </math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_POW}}||<math> \pow (\emptyset ) \;\;\defi\;\; \{ \emptyset \} </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_POW1}}||<math> \pown (\emptyset ) \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_POW1}}||<math> \pown (\emptyset ) \;\;\defi\;\; \emptyset </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_CPROD_R}}||<math> S \cprod \emptyset \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_CPROD_R}}||<math> S \cprod \emptyset \;\;\defi\;\; \emptyset </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_CPROD_L}}||<math> \emptyset \cprod S \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_CPROD_L}}||<math> \emptyset \cprod S \;\;\defi\;\; \emptyset </math>|| || A | {{RRRow}}|||{{Rulename|SIMP_COMPSET_EQUAL}}||<math> \{ x, y \qdot x = E(y) \land P(y) \mid F(x, y) \} \;\;\defi\;\; \{ y \qdot P(y) \mid F(E(y), y) \} </math>|| where <math>x</math> non free in <math>E</math> and non free in <math>P</math> || A | ||
{{RRRow}}|||{{Rulename|SIMP_COMPSET_EQUAL}}||<math> \{ | {{RRRow}}|*||{{Rulename|SIMP_COMPSET_IN}}||<math> \{ x \qdot x \in S \mid x \} \;\;\defi\;\; S </math>|| where <math>x</math> non free in <math>S</math> || A | ||
{{RRRow}}|||{{Rulename|SIMP_COMPSET_IN}}||<math> \{ x \qdot x \in S \mid x \} \;\;\defi\;\; S </math>|| where <math>x</math> non free in <math>S</math> || A | {{RRRow}}|*||{{Rulename|SIMP_COMPSET_SUBSETEQ}}||<math> \{ x \qdot x \subseteq S \mid x \} \;\;\defi\;\; \pow (S) </math>|| where <math>x</math> non free in <math>S</math> || A | ||
{{RRRow}}| ||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COMPSET_BFALSE}}||<math> \{ x \qdot \bfalse \mid x \} \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}| ||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COMPSET_BTRUE}}||<math> \{ x \qdot \btrue \mid E \} \;\;\defi\;\; \mathit{Ty} </math>|| where the type of <math>E</math> is <math>\mathit{Ty}</math> and <math>E</math> is a maplet combination of locally-bound, pairwise-distinct bound identifiers || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_COMPSET_L}}||<math> \{ x \qdot P(x) \mid E(x) \} \subseteq S \;\;\defi\;\; \forall y\qdot P(y) \limp E(y) \in S </math>|| where <math>y</math> is fresh || A | ||
{{RRRow}}| ||{{Rulename| | |||
{{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET}}||<math> 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 </math>|| where <math>x</math>, <math>y</math>, <math>\ldots</math> are not free in <math>F</math> || A | {{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET}}||<math> 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 </math>|| where <math>x</math>, <math>y</math>, <math>\ldots</math> are not free in <math>F</math> || A | ||
{{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET_ONEPOINT}}||<math> E \in \{ x \qdot P(x) \mid x \} \;\;\defi\;\; P(E) </math>|| Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate || A | {{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET_ONEPOINT}}||<math> E \in \{ x \qdot P(x) \mid x \} \;\;\defi\;\; P(E) </math>|| Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate || A | ||
{{RRRow}}|||{{Rulename|SIMP_SUBSETEQ_COMPSET_R}}||<math> S \subseteq \{ x \qdot P(x) \mid x \} \;\;\defi\;\; \forall y\qdot y \in S \limp P(y) </math>|| where <math>y</math> non free in <math> | {{RRRow}}|||{{Rulename|SIMP_SUBSETEQ_COMPSET_R}}||<math> S \subseteq \{ x \qdot P(x) \mid x \} \;\;\defi\;\; \forall y\qdot y \in S \limp P(y) </math>|| where <math>y</math> non free in <math>S, \{ x \qdot P(x) \mid x \}</math> || M | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_OVERL}}||<math> r \ovl \ldots \ovl \emptyset \ovl \ldots \ovl s \;\;\defi\;\; r \ovl \ldots \ovl s </math>|| | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OVERL}}||<math> r \ovl \ldots \ovl \emptyset \ovl \ldots \ovl s \;\;\defi\;\; r \ovl \ldots \ovl s </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KBOOL_BTRUE}}||<math> \bool (\btrue ) \;\;\defi\;\; \True </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KBOOL_BTRUE}}||<math> \bool (\btrue ) \;\;\defi\;\; \True </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KBOOL_BFALSE}}||<math> \bool (\bfalse ) \;\;\defi\;\; \False </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KBOOL_BFALSE}}||<math> \bool (\bfalse ) \;\;\defi\;\; \False </math>|| || A | ||
{{RRRow}}|||{{Rulename|DISTRI_SUBSETEQ_BUNION_SING}}||<math> S \bunion \{ F\} \subseteq T \;\;\defi\;\; S \subseteq T \land F \in T </math>|| where <math>F</math> is a single expression || M | {{RRRow}}|||{{Rulename|DISTRI_SUBSETEQ_BUNION_SING}}||<math> S \bunion \{ F\} \subseteq T \;\;\defi\;\; S \subseteq T \land F \in T </math>|| where <math>F</math> is a single expression || M | ||
{{RRRow}}| ||{{Rulename|DEF_FINITE}}||<math> \finite(S) \;\;\defi\;\; \exists n,f\qdot | {{RRRow}}|*||{{Rulename|DEF_FINITE}}||<math> \finite(S) \;\;\defi\;\; \exists n,f\qdot f\in 1\upto n \tbij S </math>|| || M | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_FINITE}}||<math> \finite (\emptyset ) \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_FINITE}}||<math> \finite (\emptyset ) \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_FINITE_SETENUM}}||<math> \finite (\{ a, \ldots , b\} ) \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_FINITE_SETENUM}}||<math> \finite (\{ a, \ldots , b\} ) \;\;\defi\;\; \btrue </math>|| || A | ||
Line 104: | Line 109: | ||
{{RRRow}}|*||{{Rulename|SIMP_FINITE_CONVERSE}}||<math> \finite (r^{-1} ) \;\;\defi\;\; \finite (r) </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_FINITE_CONVERSE}}||<math> \finite (r^{-1} ) \;\;\defi\;\; \finite (r) </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_FINITE_UPTO}}||<math> \finite (a \upto b) \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_FINITE_UPTO}}||<math> \finite (a \upto b) \;\;\defi\;\; \btrue </math>|| || A | ||
<!-- Disabled rules (some are false, need more thinking to check which) | |||
{{RRRow}}|||{{Rulename|SIMP_FINITE_UNION}}||<math>\finite(\union(S)) \;\;\defi\;\; \finite(S)\;\land\;(\forall x\qdot x\in S\limp \finite(x))</math>|| || M | |||
{{RRRow}}|||{{Rulename|SIMP_FINITE_QUNION}}||<math>\finite(\Union x\qdot P\mid E) \;\;\defi\;\; \finite(\{x\qdot P\mid E\})\;\land\;(\forall x\qdot P\limp \finite(E))</math>|| this equivalence is false: for example, the union of an infinite set of empty sets is finite; the right-to-left implication is true || M | |||
{{RRRow}}|||{{Rulename|SIMP_FINITE_BINTER_L}}||<math> \finite (S \binter T) \;\;\defi\;\; \finite (S) </math>|| || M | {{RRRow}}|||{{Rulename|SIMP_FINITE_BINTER_L}}||<math> \finite (S \binter T) \;\;\defi\;\; \finite (S) </math>|| || M | ||
{{RRRow}}|||{{Rulename|SIMP_FINITE_BINTER_R}}||<math> \finite (S \binter T) \;\;\defi\;\; \finite (T) </math>|| || M | {{RRRow}}|||{{Rulename|SIMP_FINITE_BINTER_R}}||<math> \finite (S \binter T) \;\;\defi\;\; \finite (T) </math>|| || M | ||
Line 122: | Line 130: | ||
{{RRRow}}|||{{Rulename|SIMP_FINITE_RAN}}||<math> \finite (\ran (r)) \;\;\defi\;\; \finite (r) </math>|| || M | {{RRRow}}|||{{Rulename|SIMP_FINITE_RAN}}||<math> \finite (\ran (r)) \;\;\defi\;\; \finite (r) </math>|| || M | ||
{{RRRow}}|||{{Rulename|SIMP_FINITE_DOM}}||<math> \finite (\dom (r)) \;\;\defi\;\; \finite (r) </math>|| || M | {{RRRow}}|||{{Rulename|SIMP_FINITE_DOM}}||<math> \finite (\dom (r)) \;\;\defi\;\; \finite (r) </math>|| || M | ||
{{RRRow}}|||{{Rulename|SIMP_FINITE_QINTER}}||<math> \finite (\Inter x \qdot P \mid E) \;\;\defi\;\; \exists x \qdot P \land \finite (E) </math>|| || M | {{RRRow}}|||{{Rulename|SIMP_FINITE_QINTER}}||<math> \finite (\Inter x \qdot P \mid E) \;\;\defi\;\; \exists x \qdot P \land \finite (E) </math>|| || M | ||
{{RRRow}}|||{{Rulename|SIMP_FINITE_ID}}||<math> \finite (\id) \;\;\defi\;\; \finite (S) </math>|| where <math>\id</math> has type <math>\pow(S \cprod S)</math> || A | --> | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_FINITE_ID}}||<math> \finite (\id) \;\;\defi\;\; \finite (S) </math>|| where <math>\id</math> has type <math>\pow(S \cprod S)</math> || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_FINITE_ID_DOMRES}}||<math> \finite (E \domres \id) \;\;\defi\;\; \finite (E) </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_FINITE_PRJ1}}||<math> \finite (\prjone) \;\;\defi\;\; \finite (S \cprod T) </math>|| where <math>\prjone</math> has type <math>\pow(S \cprod T \cprod S)</math> || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_FINITE_PRJ2}}||<math> \finite (\prjtwo) \;\;\defi\;\; \finite (S \cprod T) </math>|| where <math>\prjtwo</math> has type <math>\pow(S \cprod T \cprod T)</math> || A | ||
{{RRRow}}|*||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_FINITE_PRJ1_DOMRES}}||<math> \finite (E \domres \prjone) \;\;\defi\;\; \finite (E) </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_FINITE_PRJ2_DOMRES}}||<math> \finite (E \domres \prjtwo) \;\;\defi\;\; \finite (E) </math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_FINITE_NATURAL}}||<math> \finite (\nat ) \;\;\defi\;\; \bfalse </math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_FINITE_NATURAL1}}||<math> \finite (\natn ) \;\;\defi\;\; \bfalse </math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_FINITE_INTEGER}}||<math> \finite (\intg ) \;\;\defi\;\; \bfalse </math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_FINITE_BOOL}}||<math> \finite (\Bool ) \;\;\defi\;\; \btrue </math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_FINITE_LAMBDA}}||<math> \finite(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \finite(\{x\qdot P\mid E\} ) </math>|| where <math>E</math> is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., <math>E</math> is syntactically injective) and all identifiers bound by the comprehension set that occur in <math>F</math> also occur in <math>E</math> || A | |||
{{RRRow}}|*||{{Rulename|SIMP_TYPE_IN}}||<math> t \in \mathit{Ty} \;\;\defi\;\; \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression || A | {{RRRow}}|*||{{Rulename|SIMP_TYPE_IN}}||<math> t \in \mathit{Ty} \;\;\defi\;\; \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQV_BTRUE}}||<math> P \leqv \btrue \;\;\defi\;\; P </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQV_BTRUE}}||<math> P \leqv \btrue \;\;\defi\;\; P </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQV_BFALSE}}||<math> P \leqv \bfalse \;\;\defi\;\; \lnot\, P </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQV_BFALSE}}||<math> P \leqv \bfalse \;\;\defi\;\; \lnot\, P </math>|| || A | ||
{{RRRow}}|*||{{Rulename|DEF_SUBSET}}||<math> A \subset B \;\;\defi\;\; A \subseteq B \land \lnot A = B </math>|| || A | {{RRRow}}|*||{{Rulename|DEF_SUBSET}}||<math> A \subset B \;\;\defi\;\; A \subseteq B \land \lnot A = B </math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_SUBSET_R}}||<math> S \subset \emptyset \;\;\defi\;\; \bfalse </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SUBSET_R}}||<math> S \subset \emptyset \;\;\defi\;\; \bfalse </math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_SUBSET_L}}||<math> | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SUBSET_L}}||<math>\emptyset\subset S \;\;\defi\;\; \lnot\; S = \emptyset</math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_TYPE_SUBSET_L}}||<math> S \subset \mathit{Ty} \;\;\defi\;\; S \neq \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression || A | {{RRRow}}|*||{{Rulename|SIMP_TYPE_SUBSET_L}}||<math> S \subset \mathit{Ty} \;\;\defi\;\; S \neq \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
{{RRRow}}|||{{Rulename|SIMP_MULTI_SUBSET}}||<math> S \subset S \;\;\defi\;\; \bfalse </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_SUBSET}}||<math> S \subset S \;\;\defi\;\; \bfalse </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_CONSTR}}||<math> \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 </math>|| where <math>\operatorname{constr}</math> is a datatype constructor || A | |||
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_CONSTR_DIFF}}||<math> \operatorname{constr_1} (\ldots) = \operatorname{constr_2} (\ldots) \;\;\defi\;\; \bfalse </math>|| where <math>\operatorname{constr_1}</math> and <math>\operatorname{constr_2}</math> are different datatype constructors || A | |||
{{RRRow}}|*||{{Rulename|SIMP_DESTR_CONSTR}}||<math> \operatorname{destr} (\operatorname{constr} (a_1, \ldots, a_n)) \;\;\defi\;\; a_i </math>|| where <math>\operatorname{destr}</math> is the datatype destructor for the i-th argument of datatype constructor <math>\operatorname{constr}</math> || A | |||
{{RRRow}}|*||{{Rulename|DISTRI_AND_OR}}||<math> P \land (Q \lor R) \;\;\defi\;\; (P \land Q) \lor (P \land R) </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_AND_OR}}||<math> P \land (Q \lor R) \;\;\defi\;\; (P \land Q) \lor (P \land R) </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DISTRI_OR_AND}}||<math> P \lor (Q \land R) \;\;\defi\;\; (P \lor Q) \land (P \lor R) </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_OR_AND}}||<math> P \lor (Q \land R) \;\;\defi\;\; (P \lor Q) \land (P \lor R) </math>|| || M | ||
Line 155: | Line 167: | ||
{{RRRow}}|*||{{Rulename|DERIV_NOT_FORALL}}||<math> \lnot\, \forall x \qdot P \;\;\defi\;\; \exists x \qdot \lnot\, P </math>|| || M | {{RRRow}}|*||{{Rulename|DERIV_NOT_FORALL}}||<math> \lnot\, \forall x \qdot P \;\;\defi\;\; \exists x \qdot \lnot\, P </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DERIV_NOT_EXISTS}}||<math> \lnot\, \exists x \qdot P \;\;\defi\;\; \forall x \qdot \lnot\, P </math>|| || M | {{RRRow}}|*||{{Rulename|DERIV_NOT_EXISTS}}||<math> \lnot\, \exists x \qdot P \;\;\defi\;\; \forall x \qdot \lnot\, P </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DEF_IN_MAPSTO}}||<math> E \mapsto F \in S \cprod T \;\;\defi\;\; E \in S \land F \in T </math>|| || AM | |||
{{RRRow}}|*||{{Rulename|DEF_IN_MAPSTO}}||<math> E \mapsto F \in S \cprod T \;\;\defi\;\; E \in S \land F \in T </math>|| || | |||
{{RRRow}}|*||{{Rulename|DEF_IN_POW}}||<math> E \in \pow (S) \;\;\defi\;\; E \subseteq S </math>|| || M | {{RRRow}}|*||{{Rulename|DEF_IN_POW}}||<math> E \in \pow (S) \;\;\defi\;\; E \subseteq S </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DEF_IN_POW1}}||<math> E \in \pown (S) \;\;\defi\;\; E \in \pow (S) \land S \neq \emptyset </math>|| || M | {{RRRow}}|*||{{Rulename|DEF_IN_POW1}}||<math> E \in \pown (S) \;\;\defi\;\; E \in \pow (S) \land S \neq \emptyset </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DEF_SUBSETEQ}}||<math> S \subseteq T \;\;\defi\;\; \forall x \qdot x \in S \limp x \in T </math>|| | {{RRRow}}|*||{{Rulename|DEF_SUBSETEQ}}||<math> S \subseteq T \;\;\defi\;\; \forall x \qdot x \in S \limp x \in T </math>|| where <math>x</math> is not free in <math>S</math> or <math>T</math> || M | ||
{{RRRow}}|*||{{Rulename|DEF_IN_BUNION}}||<math> E \in S \bunion T \;\;\defi\;\; E \in S \lor E \in T </math>|| || M | {{RRRow}}|*||{{Rulename|DEF_IN_BUNION}}||<math> E \in S \bunion T \;\;\defi\;\; E \in S \lor E \in T </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DEF_IN_BINTER}}||<math> E \in S \binter T \;\;\defi\;\; E \in S \land E \in T </math>|| || M | {{RRRow}}|*||{{Rulename|DEF_IN_BINTER}}||<math> E \in S \binter T \;\;\defi\;\; E \in S \land E \in T </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DEF_IN_SETMINUS}}||<math> E \in S \setminus T \;\;\defi\;\; E \in S \land \lnot\,(E \in T) </math>|| || M | {{RRRow}}|*||{{Rulename|DEF_IN_SETMINUS}}||<math> E \in S \setminus T \;\;\defi\;\; E \in S \land \lnot\,(E \in T) </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DEF_IN_SETENUM}}||<math> E \in \{ A, \ldots , B\} \;\;\defi\;\; E = A \lor \ldots \lor E = B </math>|| || M | {{RRRow}}|*||{{Rulename|DEF_IN_SETENUM}}||<math> E \in \{ A, \ldots , B\} \;\;\defi\;\; E = A \lor \ldots \lor E = B </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DEF_IN_KUNION}}||<math> E \in \union (S) \;\;\defi\;\; \exists s \qdot s \in S \land E \in s </math>|| | {{RRRow}}|*||{{Rulename|DEF_IN_KUNION}}||<math> E \in \union (S) \;\;\defi\;\; \exists s \qdot s \in S \land E \in s </math>|| where <math>s</math> is fresh || M | ||
{{RRRow}}|*||{{Rulename|DEF_IN_QUNION}}||<math> E \in (\Union | {{RRRow}}|*||{{Rulename|DEF_IN_QUNION}}||<math> E \in (\Union x \qdot P(x) \mid T(x)) \;\;\defi\;\; \exists s \qdot P(s) \land E \in T(s) </math>|| where <math>s</math> is fresh || M | ||
{{RRRow}}|*||{{Rulename|DEF_IN_KINTER}}||<math> E \in \inter (S) \;\;\defi\;\; \forall s \qdot s \in S \limp E \in s </math>|| | {{RRRow}}|*||{{Rulename|DEF_IN_KINTER}}||<math> E \in \inter (S) \;\;\defi\;\; \forall s \qdot s \in S \limp E \in s </math>|| where <math>s</math> is fresh || M | ||
{{RRRow}}|*||{{Rulename|DEF_IN_QINTER}}||<math> E \in (\Inter | {{RRRow}}|*||{{Rulename|DEF_IN_QINTER}}||<math> E \in (\Inter x \qdot P(x) \mid T(x)) \;\;\defi\;\; \forall s \qdot P(s) \limp E \in T(s) </math>|| where <math>s</math> is fresh || M | ||
{{RRRow}}|*||{{Rulename|DEF_IN_UPTO}}||<math> E \in a \upto b \;\;\defi\;\; a \leq E \land E \leq b </math>|| || M | {{RRRow}}|*||{{Rulename|DEF_IN_UPTO}}||<math> E \in a \upto b \;\;\defi\;\; a \leq E \land E \leq b </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DISTRI_BUNION_BINTER}}||<math> S \bunion (T \binter U) \;\;\defi\;\; (S \bunion T) \binter (S \bunion U) </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_BUNION_BINTER}}||<math> S \bunion (T \binter U) \;\;\defi\;\; (S \bunion T) \binter (S \bunion U) </math>|| || M | ||
Line 192: | Line 203: | ||
\land& s_{n-1}\binter s_n = \emptyset | \land& s_{n-1}\binter s_n = \emptyset | ||
\end{array}</math>|| || AM | \end{array}</math>|| || AM | ||
{{RRRow}}|*||{{Rulename|SIMP_EMPTY_PARTITION}}||<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_SINGLE_PARTITION}}||<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>|| || A | |||
{{RRRow}}|*||{{Rulename|DEF_EQUAL_CARD}}||<math>\operatorname{card}(S) = k \;\;\defi\;\; \exists f \qdot f \in 1..k \tbij S</math>|| also works for <math>k = \operatorname{card}(S)</math> || M | |||
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_CARD}}||<math>\operatorname{card}(S) = \operatorname{card}(T) \;\;\defi\;\; \exists f \qdot f \in S \tbij T</math>|| || M | |||
|} | |} | ||
Latest revision as of 14:33, 13 April 2023
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 |
A | ||
* | SIMP_SPECIAL_AND_BFALSE |
A | ||
* | SIMP_MULTI_AND |
A | ||
* | SIMP_MULTI_AND_NOT |
A | ||
* | SIMP_SPECIAL_OR_BTRUE |
A | ||
* | SIMP_SPECIAL_OR_BFALSE |
A | ||
* | SIMP_MULTI_OR |
A | ||
* | SIMP_MULTI_OR_NOT |
A | ||
* | SIMP_SPECIAL_IMP_BTRUE_R |
A | ||
* | SIMP_SPECIAL_IMP_BTRUE_L |
A | ||
* | SIMP_SPECIAL_IMP_BFALSE_R |
A | ||
* | SIMP_SPECIAL_IMP_BFALSE_L |
A | ||
* | SIMP_MULTI_IMP |
A | ||
* | SIMP_MULTI_IMP_NOT_L |
A | ||
* | SIMP_MULTI_IMP_NOT_R |
A | ||
* | SIMP_MULTI_IMP_AND |
A | ||
* | SIMP_MULTI_IMP_AND_NOT_R |
A | ||
* | SIMP_MULTI_IMP_AND_NOT_L |
A | ||
* | SIMP_MULTI_EQV |
A | ||
* | SIMP_MULTI_EQV_NOT |
A | ||
* | SIMP_SPECIAL_NOT_BTRUE |
A | ||
* | SIMP_SPECIAL_NOT_BFALSE |
A | ||
* | SIMP_NOT_NOT |
AM | ||
* | SIMP_NOTEQUAL |
A | ||
* | SIMP_NOTIN |
A | ||
* | SIMP_NOTSUBSET |
A | ||
* | SIMP_NOTSUBSETEQ |
A | ||
* | SIMP_NOT_LE |
A | ||
* | SIMP_NOT_GE |
A | ||
* | SIMP_NOT_LT |
A | ||
* | SIMP_NOT_GT |
A | ||
* | SIMP_SPECIAL_NOT_EQUAL_FALSE_R |
A | ||
* | SIMP_SPECIAL_NOT_EQUAL_FALSE_L |
A | ||
* | SIMP_SPECIAL_NOT_EQUAL_TRUE_R |
A | ||
* | SIMP_SPECIAL_NOT_EQUAL_TRUE_L |
A | ||
* | SIMP_FORALL_AND |
A | ||
* | SIMP_EXISTS_OR |
A | ||
* | SIMP_EXISTS_IMP |
A | ||
* | SIMP_FORALL |
Quantified identifiers other than do not occur in | A | |
* | SIMP_EXISTS |
Quantified identifiers other than do not occur in | A | |
* | SIMP_MULTI_EQUAL |
A | ||
* | SIMP_MULTI_NOTEQUAL |
A | ||
* | SIMP_EQUAL_MAPSTO |
A | ||
* | SIMP_EQUAL_SING |
A | ||
* | SIMP_SPECIAL_EQUAL_TRUE |
A | ||
* | SIMP_TYPE_SUBSETEQ |
where is a type expression | A | |
* | SIMP_SUBSETEQ_SING |
where is a single expression | A | |
* | SIMP_SPECIAL_SUBSETEQ |
A | ||
* | SIMP_MULTI_SUBSETEQ |
A | ||
* | SIMP_SUBSETEQ_BUNION |
A | ||
* | SIMP_SUBSETEQ_BINTER |
A | ||
* | DERIV_SUBSETEQ_BUNION |
A | ||
* | DERIV_SUBSETEQ_BINTER |
A | ||
* | SIMP_SPECIAL_IN |
A | ||
* | SIMP_MULTI_IN |
A | ||
* | SIMP_IN_SING |
A | ||
* | SIMP_MULTI_SETENUM |
A | ||
* | SIMP_SPECIAL_BINTER |
A | ||
* | SIMP_TYPE_BINTER |
where is a type expression | A | |
* | SIMP_MULTI_BINTER |
A | ||
* | SIMP_MULTI_EQUAL_BINTER |
A | ||
* | SIMP_SPECIAL_BUNION |
A | ||
* | SIMP_TYPE_BUNION |
where is a type expression | A | |
* | SIMP_MULTI_BUNION |
A | ||
* | SIMP_MULTI_EQUAL_BUNION |
A | ||
* | SIMP_MULTI_SETMINUS |
A | ||
* | SIMP_SPECIAL_SETMINUS_R |
A | ||
* | SIMP_SPECIAL_SETMINUS_L |
A | ||
* | SIMP_TYPE_SETMINUS |
where is a type expression | A | |
* | SIMP_TYPE_SETMINUS_SETMINUS |
where is a type expression | A | |
* | SIMP_KUNION_POW |
A | ||
* | SIMP_KUNION_POW1 |
A | ||
* | SIMP_SPECIAL_KUNION |
A | ||
* | SIMP_SPECIAL_QUNION |
A | ||
* | SIMP_SPECIAL_KINTER |
A | ||
* | SIMP_KINTER_POW |
A | ||
* | SIMP_SPECIAL_POW |
A | ||
* | SIMP_SPECIAL_POW1 |
A | ||
* | SIMP_SPECIAL_CPROD_R |
A | ||
* | SIMP_SPECIAL_CPROD_L |
A | ||
SIMP_COMPSET_EQUAL |
where non free in and non free in | A | ||
* | SIMP_COMPSET_IN |
where non free in | A | |
* | SIMP_COMPSET_SUBSETEQ |
where non free in | A | |
* | SIMP_SPECIAL_COMPSET_BFALSE |
A | ||
* | SIMP_SPECIAL_COMPSET_BTRUE |
where the type of is and is a maplet combination of locally-bound, pairwise-distinct bound identifiers | A | |
* | SIMP_SUBSETEQ_COMPSET_L |
where is fresh | A | |
* | SIMP_IN_COMPSET |
where , , are not free in | A | |
* | SIMP_IN_COMPSET_ONEPOINT |
Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate | A | |
SIMP_SUBSETEQ_COMPSET_R |
where non free in | M | ||
* | SIMP_SPECIAL_OVERL |
A | ||
* | SIMP_SPECIAL_KBOOL_BTRUE |
A | ||
* | SIMP_SPECIAL_KBOOL_BFALSE |
A | ||
DISTRI_SUBSETEQ_BUNION_SING |
where is a single expression | M | ||
* | DEF_FINITE |
M | ||
* | SIMP_SPECIAL_FINITE |
A | ||
* | SIMP_FINITE_SETENUM |
A | ||
* | SIMP_FINITE_BUNION |
A | ||
* | SIMP_FINITE_POW |
A | ||
* | DERIV_FINITE_CPROD |
A | ||
* | SIMP_FINITE_CONVERSE |
A | ||
* | SIMP_FINITE_UPTO |
A | ||
* | SIMP_FINITE_ID |
where has type | A | |
* | SIMP_FINITE_ID_DOMRES |
A | ||
* | SIMP_FINITE_PRJ1 |
where has type | A | |
* | SIMP_FINITE_PRJ2 |
where has type | A | |
* | SIMP_FINITE_PRJ1_DOMRES |
A | ||
* | SIMP_FINITE_PRJ2_DOMRES |
A | ||
* | SIMP_FINITE_NATURAL |
A | ||
* | SIMP_FINITE_NATURAL1 |
A | ||
* | SIMP_FINITE_INTEGER |
A | ||
* | SIMP_FINITE_BOOL |
A | ||
* | SIMP_FINITE_LAMBDA |
where is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., is syntactically injective) and all identifiers bound by the comprehension set that occur in also occur in | A | |
* | SIMP_TYPE_IN |
where is a type expression | A | |
* | SIMP_SPECIAL_EQV_BTRUE |
A | ||
* | SIMP_SPECIAL_EQV_BFALSE |
A | ||
* | DEF_SUBSET |
A | ||
* | SIMP_SPECIAL_SUBSET_R |
A | ||
* | SIMP_SPECIAL_SUBSET_L |
A | ||
* | SIMP_TYPE_SUBSET_L |
where is a type expression | A | |
* | SIMP_MULTI_SUBSET |
A | ||
* | SIMP_EQUAL_CONSTR |
where is a datatype constructor | A | |
* | SIMP_EQUAL_CONSTR_DIFF |
where and are different datatype constructors | A | |
* | SIMP_DESTR_CONSTR |
where is the datatype destructor for the i-th argument of datatype constructor | A | |
* | DISTRI_AND_OR |
M | ||
* | DISTRI_OR_AND |
M | ||
* | DEF_OR |
M | ||
* | DERIV_IMP |
M | ||
* | DERIV_IMP_IMP |
M | ||
* | DISTRI_IMP_AND |
M | ||
* | DISTRI_IMP_OR |
M | ||
* | DEF_EQV |
M | ||
* | DISTRI_NOT_AND |
M | ||
* | DISTRI_NOT_OR |
M | ||
* | DERIV_NOT_IMP |
M | ||
* | DERIV_NOT_FORALL |
M | ||
* | DERIV_NOT_EXISTS |
M | ||
* | DEF_IN_MAPSTO |
AM | ||
* | DEF_IN_POW |
M | ||
* | DEF_IN_POW1 |
M | ||
* | DEF_SUBSETEQ |
where is not free in or | M | |
* | DEF_IN_BUNION |
M | ||
* | DEF_IN_BINTER |
M | ||
* | DEF_IN_SETMINUS |
M | ||
* | DEF_IN_SETENUM |
M | ||
* | DEF_IN_KUNION |
where is fresh | M | |
* | DEF_IN_QUNION |
where is fresh | M | |
* | DEF_IN_KINTER |
where is fresh | M | |
* | DEF_IN_QINTER |
where is fresh | M | |
* | DEF_IN_UPTO |
M | ||
* | DISTRI_BUNION_BINTER |
M | ||
* | DISTRI_BINTER_BUNION |
M | ||
DISTRI_BINTER_SETMINUS |
M | |||
DISTRI_SETMINUS_BUNION |
M | |||
* | DERIV_TYPE_SETMINUS_BINTER |
where is a type expression | M | |
* | DERIV_TYPE_SETMINUS_BUNION |
where is a type expression | M | |
* | DERIV_TYPE_SETMINUS_SETMINUS |
where is a type expression | M | |
DISTRI_CPROD_BINTER |
M | |||
DISTRI_CPROD_BUNION |
M | |||
DISTRI_CPROD_SETMINUS |
M | |||
* | DERIV_SUBSETEQ |
where is the type of and | M | |
* | DERIV_EQUAL |
where is the type of and | M | |
* | DERIV_SUBSETEQ_SETMINUS_L |
M | ||
* | DERIV_SUBSETEQ_SETMINUS_R |
M | ||
* | DEF_PARTITION |
AM | ||
* | SIMP_EMPTY_PARTITION |
A | ||
* | SIMP_SINGLE_PARTITION |
A | ||
* | DEF_EQUAL_CARD |
also works for | M | |
* | SIMP_EQUAL_CARD |
M |