FREEZE_THEN : thm_tactical

- STRUCTURE
- 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:then applying FREEZE_THEN f (A1 |- w) to the goal (A0 ?- t) produces the subgoal:
A0 ?- t ========= f (w |- 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.A0 ?- t =================== FREEZE_THEN f (A1 |- w) A - {w}, A1 ?- t1

- 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:IMP_RES_TAC th will generate several unneeded assumptions:
th = |- !p. a < b /\ b < p ==> a < p

which can be avoided by first ‘freezing’ the theorem, using the tactic{b < c, a < b, a < c, !p. c < p ==> b < p, !a'. a' < a ==> a' < b} ?- SUC a <= c

This prevents the variables a and b from being instantiated.FREEZE_THEN IMP_RES_TAC th

{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

HOL Kananaskis-14