HOL: Reference

VALIDATE

Tactical.VALIDATE : tactic -> tactic

Makes a tactic valid if its invalidity is due to relying on assumptions not present in the goal.

Suppose tac applied to the goal (asl,g) produces a justification that creates a theorem A |- g'. If A a not a subset of asl, then the tactic is invalid (and VALID tac (asl,g) fails, ie, raises an exception). But VALIDATE tac (asl,g) produces a subgoal list augmented by the members of A missing from asl.

If g' differs from g, both VALID tac (asl,g) and VALIDATE tac (asl,g) fail.

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 uth' is [p'] |- q

[...Lines elided...]
   5. 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)
   
   4. Incomplete goalstack:
        Initial goal:
        1 + 2 = 2 + 1
        
        Current goal:
        ∀(x,y). x + y = y + x
   
   3. Incomplete goalstack:
        Initial goal:
         0.  p ⇒ q
        ------------------------------------
             r
        
        Current goal:
        p
   
   2. Incomplete goalstack:
        Initial goal:
         0.  q
         1.  p
        ------------------------------------
             r
        
        Current goal:
         0.  q
         1.  p
        ------------------------------------
             p'
   
   1. Incomplete goalstack:
        Initial goal:
         0.  p
        ------------------------------------
             q


> e (ACCEPT_TAC uth') ;
Exception- OK..
HOL_ERR (at Tactical.VALID: Invalid tactic: theorem has bad hypothesis p') raised

> e (VALIDATE (ACCEPT_TAC uth')) ;
OK..
1 subgoal:
val it =
   
    0.  p
   ------------------------------------
        p'

Given a goal with an implication in the assumptions, one can split it into two subgoals.

[...Lines elided...]
   1. Incomplete goalstack:
        Initial goal:
         0.  p ⇒ q
        ------------------------------------
             r


> e (VALIDATE (POP_ASSUM (ASSUME_TAC o UNDISCH))) ;
OK..
2 subgoals:
val it =
   
    0.  q
   ------------------------------------
        r
   
    0.  p ⇒ q
   ------------------------------------
        p

Meanwhile, to propose a term, prove it as a subgoal and then use it to prove the goal, as is done using SUBGOAL_THEN tm ASSUME_TAC, can also be done by VALIDATE (ASSUME_TAC (ASSUME tm)))

Where a tactic tac requires certain assumptions to be present in the goal, which are not present but are capable of being proved, VALIDATE tac will conveniently set up new subgoals to prove the missing assumptions.

See also

proofManagerLib.expand, Tactical.VALID, Tactical.GEN_VALIDATE, Tactical.ADD_SGS_TAC, Tactical.SUBGOAL_THEN