(THENL) : tactic -> tactic list -> tactic

SYNOPSIS

Applies a list of tactics to the corresponding subgoals generated by a tactic.

DESCRIPTION

If t,t1,...,tn are tactics, t THENL [t1;...;tn] is a tactic which applies t to a goal, and if it does not fail, applies the tactics t1,...,tn to the corresponding subgoals, unless t completely solves the goal.

FAILURE CONDITIONS

The application of THENL to a tactic and tactic list never fails. The resulting tactic fails if t fails when applied to the goal, or if the goal list is not empty and its length is not the same as that of the tactic list, or finally if ti fails when applied to the i'th subgoal generated by t.

EXAMPLE

If we want to prove the inbuilt theorem LE_LDIV ourselves:

  # g `!a b n. ~(a = 0) /\ b <= a * n ==> b DIV a <= n`;;
  ...

we may start by proving a lemma n = (a * n) DIV a from the given hypotheses. The following step generates two subgoals:

  # e(REPEAT STRIP_TAC THEN SUBGOAL_THEN `n = (a * n) DIV a` SUBST1_TAC);;
  val it : goalstack = 2 subgoals (2 total)

   0 [`~(a = 0)`]
   1 [`b <= a * n`]

  `b DIV a <= (a * n) DIV a`

   0 [`~(a = 0)`]
   1 [`b <= a * n`]

  `n = (a * n) DIV a`

Each subgoal has a relatively short proof, but these proofs are quite different. We can combine them with the initial tactic above using THENL, so the following would solve the initial goal:

  # e(REPEAT STRIP_TAC THEN SUBGOAL_THEN `n = (a * n) DIV a` SUBST1_TAC THENL
      [ASM_SIMP_TAC[DIV_MULT]; MATCH_MP_TAC DIV_MONO THEN ASM_REWRITE_TAC[]]);;

Note that it is quite a common situation for the same tactic to be applied to all generated subgoals. In that case, you can just use THEN, e.g. in the proof of the pre-proved theorem ADD_0:

  # g `!m. m + 0 = m`;;
  ...
  # e(INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]);;
  val it : goalstack = No subgoals

USES

Applying different tactics to different subgoals.

SEE ALSO

EVERY, ORELSE, THEN.