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