ASSUME_TAC : thm_tactic

SYNOPSIS

Adds an assumption to a goal.

DESCRIPTION

Given a theorem th of the form A' |- u, and a goal, ASSUME_TAC th adds u to the assumptions of the goal.

         A ?- t
    ==============  ASSUME_TAC (A' |- u)
     A u {u} ?- t

Note that unless A' is a subset of A, this tactic is invalid. The new assumption is unlabelled; for a named assumption use LABEL_TAC.

FAILURE CONDITIONS

Never fails.

EXAMPLE

One can add an external theorem as an assumption if desired, for example so that ASM_REWRITE_TAC[] will automatically apply it. But usually the theorem is derived from some theorem-tactical, e.g. by discharging the antecedent of an implication or doing forward inference on another assumption. For example iff faced with the goal:

  # g `0 = x ==> f(2 * x) = f(x * f(x))`;;

one might not want to just do DISCH_TAC or STRIP_TAC because the assumption will be `0 = x`. One can swap it first then put it on the assumptions by:

  # e(DISCH_THEN(ASSUME_TAC o SYM));;
  val it : goalstack = 1 subgoal (1 total)

   0 [`x = 0`]

  `f (2 * x) = f (x * f x)`

after which the goal can very easily be solved:

  # e(ASM_REWRITE_TAC[MULT_CLAUSES]);;
  val it : goalstack = No subgoals

USES

Useful as a parameter to various theorem-tacticals such as X_CHOOSE_THEN, DISCH_THEN etc. when it is simply desired to add the theorem that has been deduced to the assumptions rather than used further at once.