Tactics are commands used to guide goal-directed proofs in interactive proof environments. This paper presents various possible simplifications on tactic expression and provides a justification for these simplifications, based on a precise description of the way tactics operate. In particular, this ppaer introduces a class of head-oriented tactics that are especially suited for simplification. Most of these simplifictions have been developed in an simplifier coupled with a tactic generator based on mouse interaction.
展开▼
