Reference manual / Z-related commands / Tactic application commands / simplification tac

The simplification tac built-in tactic simplifies core Z notation, performing the same inferences as the simp family of tactics defined in section simplification. It is applicable to any predicate, expression, schema text or goal. If applied to its own result, nothing changes.

The simp family of tactics are very similar to the puff family of tactics defined in section corelaws, but are intended to faithfully reflect the behaviour of the simplification tac built-in tactic.

One caveat to the above is that the rewriting aspect of commands such as absorption is not done by simplification tac.

Tactic example

"apply tactic" p e "simplification tac"

This example applies the simplification tac built-in tactic to predicate p and expression e.

IT 28-Dec-2005