GEN_VALIDATE_LT : bool -> list_tactic -> list_tactic
STRUCTURE
Tactical
SYNOPSIS
Where a list-tactic requires assumptions to be in the goal, add those assumptions as new subgoals.
DESCRIPTION
See VALIDATE_LT, which is implemented as GEN_VALIDATE_LT true.

When list-tactic ltac is applied to a goal list gl it produces a new goal list gl' and a justification. When the justification is applied to a list thl' of theorems which are the new goals gl', proved, it produces a list thl of theorems (which, for a valid list-tactic are the goals gl, proved).

But GEN_VALIDATE_LT false ltac also returns extra subgoals corresponding to the assumptions of thl.

See GEN_VALIDATE for more details.

FAILURE
Fails by design if ltac, when applied to a goal list, produces a proof which is invalid on account of proving a theorem whose conclusion differs from that of the corresponding goal.

Also fails if ltac fails when applied to the given goals.

USES
Compared with VALIDATE_LT ltac, GEN_VALIDATE_LT false ltac can produces extra, unnecessary, subgoals. But since the subgoals produced are predictable, regardless of the assumptions of the goal, which may be useful when coding compound tactics.
SEEALSO
VALID, VALID_LT, VALIDATE, VALIDATE_LT, GEN_VALIDATE
HOL  Trindemossen-1