`ASSUME_TAC : thm_tactic`
STRUCTURE
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.
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