Reference manual / Z-related commands / Refinement commands / remove invariant

This command is part of the experimental refinement editor.

The remove invariant command refines a specification statement to replace its invariant by true. It applies the following inference rule of the refinement calculus.

\vdash? P \implies I      \vdash? Q \implies I      \vdash? \specstmt F[P, Q]
\vdash? \specstmt F[P,I,Q]

No code is implicitly generated by this refinement rule.

The remove invariant command is applicable when a specification statement \specstmt F[P,I,Q] in a goal is inspected, except where I is already true.

Tactic example

"remove invariant" p

This example applies the remove invariant command to specification statement p.

IT 20-Nov-2000