GEN_VALIDATE
Tactical.GEN_VALIDATE : bool -> tactic -> tactic
Where a tactic requires assumptions to be in the goal, add those assumptions as new subgoals.
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] |- r
[...Lines elided...]
4. Incomplete goalstack:
Initial goal:
∃R. WF R ∧ (∀rst x ord. R (ord,FILTER (ord x) rst) (ord,x::rst)) ∧
∀rst x ord. R (ord,FILTER ($¬ ∘ ord x) rst) (ord,x::rst)
3. Incomplete goalstack:
Initial goal:
1 + 2 = 2 + 1
Current goal:
∀(x,y). x + y = y + x
2. Incomplete goalstack:
Initial goal:
0. p ⇒ q
------------------------------------
r
Current goal:
p
1. Incomplete goalstack:
Initial goal:
0. q
1. p
------------------------------------
r
> e (VALIDATE (ACCEPT_TAC uthr')) ;
OK..
1 subgoal:
val it =
0. q
1. p
------------------------------------
p'
but, instead of that,
> e (GEN_VALIDATE false (ACCEPT_TAC uthr')) ;
OK..
2 subgoals:
val it =
0. q
1. p
------------------------------------
q
0. q
1. p
------------------------------------
p'
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.