Next: Writing Simple Tactics Up: Proof Tactics Previous: Refinement Tactics

# Transformation Tactics

Whereas refinement tactics take only goals as arguments and return proofs, transformation  tactics take proofs as arguments and return proofs. Transformation tactics can perform much more global analysis and change to proofs than can refinement tactics. These tactics, for instance, can complete or expand an unfinished proof, produce a new proof that is analogous to the given proof and perform various optimizations to the proof such as replacing subproofs with more elegant or concise ones, to name a few of the uses to which they have been put.

A user invokes a transformation tactic by editing the theorem of interest and traversing the proof until the goal heading the desired subproof is displayed. The user then types , and will prompt for the name of the transformation tactic which is to be applied. The tactic is applied to the proof consisting of the current goal and anything that is below it, that is, any subgoals and proofs below the subgoals. The transformation tactic, if it succeeds, will return a proof which has the same goal as the argument proof tree. Unlike those of refinement tactics, the name of the transformation tactic is not entered into the proof; the tactic serves as an operation on proofs, transforming one proof to another. Upon termination the proof returned may bear little resemblance to the original proof, except that a transformation tactic cannot change the proof above the root of the argument, nor can it change the goal of the root of the subproof. The only exception to this rule is if the subproof is the whole proof---the tactic was called from the top goal. In this case the transformation tactic may replace the goal of the proof; thus a transformation tactic can map one theorem into another. These constraints are enforced by the implementation and need not be the concern of the tactic designer or user.

Next: Writing Simple Tactics Up: Proof Tactics Previous: Refinement Tactics

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995