/usr/share/hol88-2.02.19940316/help/ENTRIES/expandf.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 | \DOC expandf
\TYPE {expandf : (tactic -> void)}
\SYNOPSIS
Applies a tactic to the current goal, stacking the resulting subgoals.
\DESCRIBE
The function {expandf} is a faster version of {expand}. It does not use a
validated version of the tactic. That is, no check is made that the
justification of the tactic does prove the goal from the subgoals it generates.
If an invalid tactic is used, the theorem ultimately proved may not match the
goal originally set. Alternatively, failure may occur when the justifications
are applied in which case the theorem would not be proved. For a description of
the subgoal package, see under {set_goal}.
\FAILURE
Calling {expandf 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. If an invalid tactic,
whose justification actually fails, has been used earlier in the proof,
{expandf tac} may succeed in applying {tac} and apparently prove the current
goal. It may then fail as it applies the justifications of the tactics applied
earlier.
\EXAMPLE
{
#g "HD[1;2;3] = 1";;
"HD[1;2;3] = 1"
() : void
#expandf (REWRITE_TAC[HD;TL]);;
OK..
goal proved
|- HD[1;2;3] = 1
Previous subproof:
goal proved
() : void
}
\noindent The following example shows how the use of an invalid tactic can
yield a theorem which does not correspond to the goal set.
{
#set_goal([],"1=2");;
"1 = 2"
() : void
#expandf (REWRITE_TAC[ASSUME "1=2"]);;
OK..
goal proved
. |- 1 = 2
Previous subproof:
goal proved
() : void
}
\noindent The proof assumed something which was not on the assumption list.
This assumption appears in the assumption list of the theorem proved, even
though it was not in the goal. An attempt to perform the proof using {expand}
fails. The validated version of the tactic detects that the justification
produces a theorem which does not correspond to the goal set. It therefore
fails.
\USES
Saving CPU time when doing goal-directed proofs, since the extra validation is
not done. Redoing proofs quickly that are already known to work.
\COMMENTS
The CPU time saved may cause misery later. If an invalid tactic is used, this
will only be discovered when the proof has apparently been finished and the
justifications are applied.
\SEEALSO
b, backup, backup_limit, e, expand, g, get_state, p, print_state, r,
rotate, save_top_thm, set_goal, set_state, top_goal, top_thm, VALID.
\ENDDOC
|