TRANS_TAC
Tactic.TRANS_TAC : thm -> term -> tactic
Applies transitivity theorem to goal with chosen intermediate term.
When applied to a 'transitivity' theorem, i.e. one of the form
|- !xs. R1 x y /\ R2 y z ==> R3 x z
and a term t, TRANS_TAC produces a tactic that reduces a goal with
conclusion of the form R3 s u to one with conclusion
R1 s t /\ R2 t u.
A ?- R3 s u
======================== TRANS_TAC (|- !xs. R1 x y /\ R2 y z ==> R3 x z) `t`
A ?- R1 s t /\ R2 t u
Example
Consider the simple inequality goal:
> g `n < (m + 2) * (n + 1)`;
We can use the following transitivity theorem
> LESS_EQ_LESS_TRANS;
val it = |- !m n p. m <= n /\ n < p ==> m < p: thm
# e (TRANS_TAC LESS_EQ_LESS_TRANS ``1 * (n + 1)``);
OK..
1 subgoal:
val it =
n <= 1 * (n + 1) /\ 1 * (n + 1) < (m + 2) * (n + 1)
: proof
Failure
Fails unless the input theorem is of the expected form (some of the
relations R1, R2 and R3 may be, and often are, the same) and the
conclusion matches the goal, in the usual sense of higher-order
matching.
Comments
The effect of TRANS_TAC th t can often be replicated by the more
primitive tactic sequence MATCH_MP_TAC th THEN EXISTS_TAC t. The use
of TRANS_TAC is not only less verbose, but it is also more general in
that it ensures correct type-instantiation of the theorem, whereas in
highly polymorphic theorems the use of MATCH_MP_TAC may leave the
wrong types for the subsequent EXISTS_TAC step.
If R1 x y, etc. are actually overloads of negated terms, e.g.,
~(R1' y x), TRANS_TAC can still work. Such overloads are common for
many definitions of "less" as an overload of "not less-or-equal",
i.e. x < y is an overload of ~(y <= x).