GEN_VALIDATE : bool -> tactic -> tactic

- STRUCTURE
- SYNOPSIS
- Where a tactic requires assumptions to be in the goal, add those assumptions as new subgoals.
- DESCRIPTION
- See VALIDATE, which is implemented as GEN_VALIDATE true.
Suppose tac applied to the goal (asl,g) produces a justification that creates a theorem A |- g'. Then GEN_VALIDATE false adds new subgoals for members of A, regardless of whether they are present in asl.

- FAILURE
- Fails by design if tac, when applied to a goal, produces a proof which is invalid on account of proving a theorem whose conclusion differs from that of the goal.
Also fails if tac fails when applied to the given goal.

- EXAMPLE
- For example, where theorem uthr' is [p', q] |- rbut, instead of that,
1 subgoal: val it = r ------------------------------------ 0. p 1. q > e (VALIDATE (ACCEPT_TAC uthr')) ; OK.. 1 subgoal: val it = p' ------------------------------------ p : proof

> e (GEN_VALIDATE false (ACCEPT_TAC uthr')) ; OK.. 2 subgoals: val it = q ------------------------------------ 0. p 1. q p' ------------------------------------ 0. p 1. q

- USES
- Use GEN_VALIDATE false rather than VALIDATE when programming compound tactics if you want to know what the resulting subgoals will be, regardless of what the assumptions of the goal are.
- SEEALSO

HOL Kananaskis-13