1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
\DOC e
\TYPE {e : tactic -> goalstack}
\SYNOPSIS
Applies a tactic to the current goal, stacking the resulting subgoals.
\DESCRIBE
The function {e} is part of the subgoal package. It applies a tactic to the
current goal to give a new proof state. The previous state is stored on the
backup list. If the tactic produces subgoals, the new proof state is formed
from the old one by adding a new level consisting of its subgoals.
The tactic applied is a validating version of the tactic given. It ensures that
the justification of the tactic does provide a proof of the goal from the
subgoals generated by the tactic. It will cause failure if this is not so. The
tactical {VALID} performs this validation.
For a description of the subgoal package, see {set_goal}.
\FAILURE
{e tac} fails if the tactic {tac} fails for the top goal. It will diverge if
the tactic diverges for the goal. It will fail if there are no unproven goals.
This could be because no goal has been set using {set_goal} or because the last
goal set has been completely proved. It will also fail in cases when the tactic
is invalid.
\EXAMPLE
{
# g `(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])`;;
val it : goalstack = 1 subgoal (1 total)
`HD [1; 2; 3] = 1 /\ TL [1; 2; 3] = [2; 3]`
# e CONJ_TAC;;
val it : goalstack = 2 subgoals (2 total)
`TL [1; 2; 3] = [2; 3]`
`HD [1; 2; 3] = 1`
# e (REWRITE_TAC[HD]);;
val it : goalstack = 1 subgoal (1 total)
`TL [1; 2; 3] = [2; 3]`
# e (REWRITE_TAC[TL]);;
val it : goalstack = No subgoals
}
\USES
Doing a step in an interactive goal-directed proof.
\SEEALSO
b, g, p, r, set_goal, top_goal, top_thm.
\ENDDOC
|
