----------------------------------------------------------------------
ASSUME_TAC                                                    (Tactic)
----------------------------------------------------------------------
ASSUME_TAC : thm_tactic

SYNOPSIS
Adds an assumption to a goal.

KEYWORDS
tactic, assumption.

DESCRIBE
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.

FAILURE
Never fails.

EXAMPLE
Given a goal {g} of the form {{x = y, y = z} ?- P},
where {x}, {y} and {z} have type {:'a},
the theorem {x = y, y = z |- x = z} can, first, be inferred by
forward proof

   let val eq1 = Term `(x:'a) = y`
       val eq2 = Term `(y:'a) = z`
   in
   TRANS (ASSUME eq1) (ASSUME eq2)
   end;

and then added to the assumptions. This process requires
the explicit text of the assumptions, as well as invocation of
the rule {ASSUME}:

   let val eq1 = Term `(x:'a) = y`
       val eq2 = Term `(y:'a) = z`
       val goal = ([eq1,eq2],Parse.Term `P:bool`)
   in
   ASSUME_TAC (TRANS (ASSUME eq1) (ASSUME eq2)) goal
   end;

   val it = ([([`x = z`, `x = y`, `y = z`], `P`)], fn) : tactic_result

This is the naive way of manipulating assumptions; there are more
advanced proof styles (more elegant and less transparent) that achieve the
same effect, but this is a perfectly correct technique in itself.

Alternatively, the axiom {EQ_TRANS} could be added to the
assumptions of {g}:

   let val eq1 = Term `(x:'a) = y`
       val eq2 = Term `(y:'a) = z`
       val goal = ([eq1,eq2], Term `P:bool`)
   in
   ASSUME_TAC EQ_TRANS goal
   end;

   val it =
     ([([`!x y z. (x = y) /\ (y = z) ==> (x = z)`,
         `x = y`,`y = z`],`P`)],fn) : tactic_result


A subsequent resolution (see {RES_TAC}) would then be able to add
the assumption {x = z} to the subgoal shown above. (Aside from purposes of
example, it would be more usual to use {IMP_RES_TAC} than {ASSUME_TAC}
followed by {RES_TAC} in this context.)

USES
{ASSUME_TAC} is the naive way of manipulating assumptions (i.e. without
recourse to advanced tacticals); and it is useful for enriching the assumption
list with lemmas as a prelude to resolution ({RES_TAC}, {IMP_RES_TAC}),
rewriting with assumptions ({ASM_REWRITE_TAC} and so on), and other operations
involving assumptions.

SEEALSO
Tactic.ACCEPT_TAC, Tactic.IMP_RES_TAC, Tactic.RES_TAC,
Tactic.STRIP_ASSUME_TAC.

----------------------------------------------------------------------