GEN_VALIDATE_LT : bool -> list_tactic -> list_tactic

- STRUCTURE
- 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

HOL Kananaskis-13