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.

See also

Tactical.VALID, Tactical.VALIDATE, Tactical.ADD_SGS_TAC