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.Note that unless A' is a subset of A, this tactic is invalid.
A ?- t ============== ASSUME_TAC (A' |- u) A u {u} ?- t

- 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 proofand 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` in TRANS (ASSUME eq1) (ASSUME eq2) end;

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

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

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

- 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

HOL Kananaskis-14