CADiZ

Reference manual / Z-related commands / In situ replacement commands / normalization


The normalization command extracts the property that is implicit in a declaration, reducing the declaration to be in terms of the carrier set of the underlying type (unlike predication).

...; i : e; ... | p   \trarrow   ...; i : carrier (\power-1 (\tau e)); ... | i \in e \land p
...; i == e; ... | p   \trarrow   ...; i : carrier (\tau e); ... | i = e \land p
...; e; ... | p   \trarrow   ...; carrier (\power-1 (\tau e)); ... | e \land p

In the first two rules, it must be the name of the declaration that is inspected. In the last rule, that of a schema declaration, it must be the schema inclusion declaration that is inspected, not the schema expression within it - an extra click of button 1 is needed. The extracted property is that schema expression used as a predicate.

The normalization command can also be applied to declarations in the hypothesis part of a goal, the new predicate being generated as the first antecedent.

The normalization command can also be applied to a quantified predicate with a schema text whose | part is not true: the predicate of that | part is logically combined with the predicate in the @ part.

\forall ds | p1 @ p2   \trarrow   \forall ds @ p1 \implies p2
\exists ds | p1 @ p2   \trarrow   \exists ds @ p1 \land p2
\exists1 ds | p1 @ p2   \trarrow   \exists1 ds @ p1 \land p2

See also denormalization.

Tactic example

"normalization" d1 d2

This example applies the normalization command to declarations d1 and d2.


IT 22-Feb-2005