`Freezes' a theorem to prevent instantiation of its free variables.
DESCRIPTION
FREEZE_THEN expects a tactic-generating function f:thm->tactic
and a theorem (A1 |- w) as arguments. The tactic-generating function f
is applied to the theorem (w |- w). If this tactic generates the subgoal:
A ?- t
========= f (w |- w)
A ?- t1
then applying FREEZE_THEN f (A1 |- w)
to the goal (A ?- t) produces the subgoal:
A ?- t
========= FREEZE_THEN f (A1 |- w)
A ?- t1
Since the term w is a hypothesis of the argument to the
function f, none of the free variables present in w may be
instantiated or generalized. The hypothesis is discharged by
PROVE_HYP upon the completion of the proof of the subgoal.
FAILURE CONDITIONS
Failures may arise from the tactic-generating function. An invalid
tactic arises if the hypotheses of the theorem are not
alpha-convertible to assumptions of the goal.
USES
Used in serious proof hacking to limit the matches achievable by rewriting etc.