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.

Thu Sep 14 08:45:18 EDT 1995