## Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License |
## 3.4.8 Simplifying ProofsProofs consists of trees where each node is a proof step. Storing or investigating a proof consists in saving or reviewing all these nodes. With post tactics activated, some unneeded steps might be added to the proof, after each manual step. Indeed, the post tactics try to apply some rewriting and inference rules which are themselves grouped into proof steps. When the proof step concern some useless hypotheses, for example, the applied rules are not useful in the proof. They can even appear cumbersome regarding storage or later investigation of the proofs. Hence, it is recommended to apply simplification before storage of huge proofs and/or proofs involving extensively post tactics. ## 3.4.8.1 Selecting simplification inputIn any view, right-clicking an Event-B project or file will display a popup menu with a Simplify Proof(s) option. If several files or projects (or both) are selected, simplification will apply to all of them. ## 3.4.8.2 Automatic simplification optionIt is possible to automatically launch the simplification on proof save. However, because this task can be performance consuming this feature is disabled by default. It can be enabled by selecting Window Preferences Event-B Sequent Prover Simplify complete proofs when saving. |