FREEZE_THEN : thm_tactical
STRUCTURE
Tactic
SYNOPSIS
‘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
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.
EXAMPLE
Given the goal ([ "b < c"; "a < b" ], "(SUC a) <= c"), and the specialized variant of the theorem LESS_TRANS: 
   th = |- !p. a < b /\ b < p ==> a < p
IMP_RES_TAC th will generate several unneeded assumptions: 
   {b < c, a < b, a < c, !p. c < p ==> b < p, !a'. a' < a ==> a' < b}
       ?- (SUC a) <= c
which can be avoided by first ‘freezing’ the theorem, using the tactic 
   FREEZE_THEN IMP_RES_TAC th
This prevents the variables a and b from being instantiated. 
   {b < c, a < b, a < c} ?- (SUC a) <= c

USES
Used in serious proof hacking to limit the matches achievable by resolution and rewriting.
SEEALSO
ASSUME, IMP_RES_TAC, PROVE_HYP, RES_TAC, REWR_CONV
HOL  Kananaskis-10