1\DOC VALIDATE 2 3\TYPE {VALIDATE : tactic -> tactic} 4 5\SYNOPSIS 6Makes a tactic valid if its invalidity is due to relying on assumptions not 7present in the goal. 8 9\DESCRIBE 10Suppose {tac} applied to the goal {(asl,g)} produces a justification that 11creates a theorem {A |- g'}. 12If {A} a not a subset of {asl}, then the tactic is invalid 13(and {VALID tac (asl,g)} fails, ie, raises an exception). 14But {VALIDATE tac (asl,g)} produces a subgoal list augmented by the 15members of {A} missing from {asl}. 16 17If {g'} differs from {g}, both {VALID tac (asl,g)} and {VALIDATE tac (asl,g)} 18fail. 19 20\FAILURE 21Fails by design if {tac}, when applied to a goal, 22produces a proof which is invalid on account of proving 23a theorem whose conclusion differs from that of the goal. 24 25Also fails if {tac} fails when applied to the given goal. 26 27\EXAMPLE 28For example, where theorem {uth'} is {[p'] |- q} 29 30{ 311 subgoal: 32val it = 33 34q 35------------------------------------ 36 p 37: 38 proof 39 40> e (ACCEPT_TAC uth') ; 41OK.. 42 43Exception raised at Tactical.VALID: 44Invalid tactic [...] 45 46> e (VALIDATE (ACCEPT_TAC uth')) ; 47OK.. 481 subgoal: 49val it = 50 51p' 52------------------------------------ 53 p 54: 55 proof 56} 57 58Given a goal with an implication in the assumptions, 59one can split it into two subgoals. 60{ 611 subgoal: 62val it = 63 64r 65------------------------------------ 66 p ==> q 67: 68 proof 69 70> e (VALIDATE (POP_ASSUM (ASSUME_TAC o UNDISCH))) ; 71 72OK.. 732 subgoals: 74val it = 75 76r 77------------------------------------ 78 q 79 80p 81------------------------------------ 82 p ==> q 83 842 subgoals 85: 86 proof 87} 88Meanwhile, to propose a term, prove it as a subgoal and then use it to prove 89the goal, as is done using {SUBGOAL_THEN tm ASSUME_TAC}, 90can also be done by {VALIDATE (ASSUME_TAC (ASSUME tm)))} 91 92 93\USES 94Where a tactic {tac} requires certain assumptions to be present in the goal, 95which are not present but are capable of being proved, 96{VALIDATE tac} will conveniently set up new subgoals to prove the missing 97assumptions. 98 99\SEEALSO 100proofManagerLib.expand, Tactical.VALID, Tactical.GEN_VALIDATE, 101Tactical.ADD_SGS_TAC, Tactical.SUBGOAL_THEN. 102 103\ENDDOC 104