TRANS_TAC : thm -> term -> tactic

SYNOPSIS

Applies transitivity theorem to goal with chosen intermediate term.

DESCRIPTION

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

  # LET_TRANS;;
  val it : thm = |- !m n p. m <= n /\ n < p ==> m < p

  # e(TRANS_TAC LET_TRANS `1 * (n + 1)`);;
  val it : goalstack = 1 subgoal (1 total)

  `n <= 1 * (n + 1) /\ 1 * (n + 1) < (m + 2) * (n + 1)`

FAILURE CONDITIONS

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.

SEE ALSO

MATCH_MP_TAC, TRANS.