/usr/share/hol88-2.02.19940316/help/ENTRIES/VALID.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 | \DOC VALID
\TYPE {VALID : (tactic -> tactic)}
\SYNOPSIS
Tries to ensure that a tactic is valid.
\KEYWORDS
tactical.
\DESCRIBE
For any tactic {T}, the application {VALID T} gives a new tactic which when
applied to a goal, checks that {T} as applied to that goal is valid, i.e. the
subgoals produced, if proved, can be used by the justification function given
by {T} to construct a theorem corresponding to the original goal.
This check is performed by actually creating, using {mk_thm}, theorems
corresponding to the subgoals, and seeing if the result of applying the
justification function to them gives a theorem corresponding to the original
goal. If it does, then {VALID T} simply applies {T}, and if not it fails.
The method by which theorems are created from goals can be changed by rebinding
the assignable variable {chktac} - see its documentation entry for details.
\FAILURE
The application of {VALID} to a tactic never fails. The resulting
tactic fails either if the original tactic fails or is invalid.
\COMMENTS
The use of {mk_thm} is a possible, though improbable, loophole
in the general security of the theorem abstract type, since it does
create possibly spurious theorems; however these should remain anonymous
in the absence of other bugs in the system.
By default the same validity checking procedure, {check_valid}, is
invoked by the subgoal package, but it can be switched off.
It is not checked whether the tactic is strongly valid, i.e. the
subgoals are provable; clearly this is not possible in general.
\SEEALSO
CHANGED_TAC, check_valid, chktac, e, expand, TRY.
\ENDDOC
|