1\DOC expandf
2
3\TYPE {expandf : (tactic -> unit)}
4
5\SYNOPSIS
6Applies a tactic to the current goal, stacking the resulting subgoals.
7
8\DESCRIBE
9The function {expandf} is a faster version of {expand}. It does not use a
10validated version of the tactic. That is, no check is made that the
11justification of the tactic does prove the goal from the subgoals it generates.
12If an invalid tactic is used, the theorem ultimately proved  may not match the
13goal originally set. Alternatively, failure may occur when the justifications
14are applied in which case the theorem would not be proved. For a description of
15the subgoal package, see under {set_goal}.
16
17\FAILURE
18Calling {expandf tac} fails if the tactic {tac} fails for the top goal. It will
19diverge if the tactic diverges for the goal. It will fail if there are no
20unproven goals. This could be because no goal has been set using {set_goal} or
21because the last goal set has been completely proved. If an invalid tactic,
22whose justification actually fails, has been used earlier in the proof,
23{expandf tac} may succeed in applying {tac} and apparently prove the current
24goal. It may then fail as it applies the justifications of the tactics applied
25earlier.
26
27\EXAMPLE
28{
29   - g `HD[1;2;3] = 1`;
30
31   `HD[1;2;3] = 1`
32
33   () : void
34
35   - expandf (REWRITE_TAC[HD;TL]);;
36   OK..
37   goal proved
38   |- HD[1;2;3] = 1
39
40   Previous subproof:
41   goal proved
42   () : void
43}
44The following example shows how the use of an invalid tactic can
45yield a  theorem which does not correspond to the  goal set.
46{
47   - set_goal([], Term `1=2`);
48   `1 = 2`
49
50   () : void
51
52   - expandf (REWRITE_TAC[ASSUME (Term`1=2`)]);
53   OK..
54   goal proved
55   . |- 1 = 2
56
57   Previous subproof:
58   goal proved
59   () : void
60}
61The proof assumed something which was not on the assumption list.
62This assumption appears in the assumption list of the theorem proved, even
63though it was not in the goal. An attempt to perform the proof using {expand}
64fails. The validated version of the tactic detects that the justification
65produces a theorem which does not correspond to the goal set. It therefore
66fails.
67
68\USES
69Saving CPU time when doing goal-directed proofs, since the extra validation is
70not done. Redoing proofs quickly that are already known to work.
71
72\COMMENTS
73The CPU time saved may cause  misery later. If an invalid tactic is used, this
74will only be discovered when the proof has apparently been finished and the
75justifications are applied.
76
77\SEEALSO
78proofManagerLib.set_goal, proofManagerLib.restart,
79proofManagerLib.backup,proofManagerLib.restore, proofManagerLib.save,
80proofManagerLib.set_backup,proofManagerLib.expand, proofManagerLib.expandf,
81proofManagerLib.p,proofManagerLib.top_thm, proofManagerLib.top_goal.
82
83\ENDDOC
84