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