1\DOC ASSUME_TAC 2 3\TYPE {ASSUME_TAC : thm_tactic} 4 5\SYNOPSIS 6Adds an assumption to a goal. 7 8\KEYWORDS 9tactic, assumption. 10 11\DESCRIBE 12Given a theorem {th} of the form {A' |- u}, and a goal, {ASSUME_TAC th} 13adds {u} to the assumptions of the goal. 14{ 15 A ?- t 16 ============== ASSUME_TAC (A' |- u) 17 A u {u} ?- t 18} 19Note that unless {A'} is a subset of {A}, this tactic is invalid. 20 21\FAILURE 22Never fails. 23 24\EXAMPLE 25Given a goal {g} of the form {{x = y, y = z} ?- P}, 26where {x}, {y} and {z} have type {:'a}, 27the theorem {x = y, y = z |- x = z} can, first, be inferred by 28forward proof 29{ 30 let val eq1 = Term `(x:'a) = y` 31 val eq2 = Term `(y:'a) = z` 32 in 33 TRANS (ASSUME eq1) (ASSUME eq2) 34 end; 35} 36and then added to the assumptions. This process requires 37the explicit text of the assumptions, as well as invocation of 38the rule {ASSUME}: 39{ 40 let val eq1 = Term `(x:'a) = y` 41 val eq2 = Term `(y:'a) = z` 42 val goal = ([eq1,eq2],Parse.Term `P:bool`) 43 in 44 ASSUME_TAC (TRANS (ASSUME eq1) (ASSUME eq2)) goal 45 end; 46 47 val it = ([([`x = z`, `x = y`, `y = z`], `P`)], fn) : tactic_result 48} 49This is the naive way of manipulating assumptions; there are more 50advanced proof styles (more elegant and less transparent) that achieve the 51same effect, but this is a perfectly correct technique in itself. 52 53Alternatively, the axiom {EQ_TRANS} could be added to the 54assumptions of {g}: 55{ 56 let val eq1 = Term `(x:'a) = y` 57 val eq2 = Term `(y:'a) = z` 58 val goal = ([eq1,eq2], Term `P:bool`) 59 in 60 ASSUME_TAC EQ_TRANS goal 61 end; 62 63 val it = 64 ([([`!x y z. (x = y) /\ (y = z) ==> (x = z)`, 65 `x = y`,`y = z`],`P`)],fn) : tactic_result 66 67} 68A subsequent resolution (see {RES_TAC}) would then be able to add 69the assumption {x = z} to the subgoal shown above. (Aside from purposes of 70example, it would be more usual to use {IMP_RES_TAC} than {ASSUME_TAC} 71followed by {RES_TAC} in this context.) 72 73\USES 74{ASSUME_TAC} is the naive way of manipulating assumptions (i.e. without 75recourse to advanced tacticals); and it is useful for enriching the assumption 76list with lemmas as a prelude to resolution ({RES_TAC}, {IMP_RES_TAC}), 77rewriting with assumptions ({ASM_REWRITE_TAC} and so on), and other operations 78involving assumptions. 79 80\SEEALSO 81Tactic.ACCEPT_TAC, Tactic.IMP_RES_TAC, Tactic.RES_TAC, Tactic.STRIP_ASSUME_TAC. 82\ENDDOC 83