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