Example Transformation Tactics

To illustrate the use of transformation  tactics we examine a pair of tactics, mark  and copy , that can be used to copy proofs. To use these tactics the user locates the proof he wants to copy and invokes the mark tactic as a transformation tactic. He then locates the goal where he wants the proof inserted and invokes copy as a transformation tactic. The application of mark does not change the proof and records the proof in the ML state so that it is available when the copy tactic is used. Note that the goal of the proof where the copied proof is inserted cannot be changed by the copy tactic.

The mark tactic is defined as follows. The variable saved_ proof is a reference variable of type proof.

    let mark goal_proof = 
        (saved_proof := goal_proof;
         IDTAC goal_proof
        );;

The basis of the copy tactic is a verbatim copy of the saved proof. This is accomplished by recursively traversing the saved proof and refining using the refinement rule of the saved proof. The following is a first approximation of the copy tactic.

    letrec copy_pattern pattern goal =
        (refine (refinement pattern)
         THENL (map copy_pattern (children pattern))
        ) goal;;
    
    
    let copy goal =  copy_pattern saved_proof goal;;

This version of copy will fail if the saved proof is incomplete since the selector refinement fails if applied to a proof without a refinement rule. To correct this deficiency we define a predicate is_refined and change copy_pattern to apply immediate where there is no refinement in the saved proof.

    letrec copy_pattern pattern goal =
        if is_refined pattern then
            (refine (refinement pattern)
             THENL (map copy_pattern (children pattern))
            ) goal
        else
            immediate goal;;

With this as a basis any number of more general proof--copying tactics can be defined. For example, the following version of copy looks up the actual formula being referenced in elimination rules, rather than just the index in the hypothesis list, and locates the corresponding hypothesis in the context where the proof is being inserted. Furthermore, if one of the refinements from the pattern fails in the new context then immediate is tried.

    letrec copy_pattern pattern goal =
        if is_refined pattern then
            (refine (adjust_elim_rules pattern goal)
                THENL (map copy_pattern (children pattern))
             ORELSE immediate
            ) goal
        else
            immediate goal;;

The function adjust_elim_rules checks if the refinement is an elimination rule. If the refinement is not an elimination, the function returns the value of the rule unchanged. If it is an elimination rule, the tactic looks up the hypothesis in the pattern indexed by the rule and finds the index of an equal hypothesis in the hypothesis set of the goal. In this case the value returned is the old elimination rule with the index changed to be the index in the hypothesis set of the goal rather than the pattern.