3.4.8 Simplifying Proofs

Proofs 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 input

In 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 option

It 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.