author  paulson 
Tue, 22 Jul 1997 11:14:18 +0200  
changeset 3538  ed9de44032e0 
parent 2807  04c080e60f31 
child 3561  329441e7eeee 
permissions  rwrr 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

1 
(* Title: tctical 
0  2 
ID: $Id$ 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

6 
Tacticals 

7 
*) 

8 

2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

9 
infix 1 THEN THEN'; 
0  10 
infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE'; 
671  11 
infix 0 THEN_ELSE; 
12 

0  13 

14 
signature TACTICAL = 

15 
sig 

1502  16 
type tactic (* = thm > thm Sequence.seq*) 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

17 
val all_tac : tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

18 
val ALLGOALS : (int > tactic) > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

19 
val APPEND : tactic * tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

20 
val APPEND' : ('a > tactic) * ('a > tactic) > 'a > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

21 
val CHANGED : tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

22 
val COND : (thm > bool) > tactic > tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

23 
val DETERM : tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

24 
val EVERY : tactic list > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

25 
val EVERY' : ('a > tactic) list > 'a > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

26 
val EVERY1 : (int > tactic) list > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

27 
val FILTER : (thm > bool) > tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

28 
val FIRST : tactic list > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

29 
val FIRST' : ('a > tactic) list > 'a > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

30 
val FIRST1 : (int > tactic) list > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

31 
val FIRSTGOAL : (int > tactic) > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

32 
val goals_limit : int ref 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

33 
val INTLEAVE : tactic * tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

34 
val INTLEAVE' : ('a > tactic) * ('a > tactic) > 'a > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

35 
val METAHYPS : (thm list > tactic) > int > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

36 
val no_tac : tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

37 
val ORELSE : tactic * tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

38 
val ORELSE' : ('a > tactic) * ('a > tactic) > 'a > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

39 
val pause_tac : tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

40 
val print_tac : tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

41 
val REPEAT : tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

42 
val REPEAT1 : tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

43 
val REPEAT_DETERM_N : int > tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

44 
val REPEAT_DETERM : tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

45 
val REPEAT_DETERM1 : tactic > tactic 
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

46 
val REPEAT_DETERM_FIRST: (int > tactic) > tactic 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

47 
val REPEAT_DETERM_SOME: (int > tactic) > tactic 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

48 
val REPEAT_FIRST : (int > tactic) > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

49 
val REPEAT_SOME : (int > tactic) > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

50 
val SELECT_GOAL : tactic > int > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

51 
val SOMEGOAL : (int > tactic) > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

52 
val STATE : (thm > tactic) > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

53 
val strip_context : term > (string * typ) list * term list * term 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

54 
val SUBGOAL : ((term*int) > tactic) > int > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

55 
val suppress_tracing : bool ref 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

56 
val THEN : tactic * tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

57 
val THEN' : ('a > tactic) * ('a > tactic) > 'a > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

58 
val THEN_ELSE : tactic * (tactic*tactic) > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

59 
val traced_tac : (thm > (thm * thm Sequence.seq) option) > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

60 
val tracify : bool ref > tactic > thm > thm Sequence.seq 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

61 
val trace_REPEAT : bool ref 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

62 
val TRY : tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

63 
val TRYALL : (int > tactic) > tactic 
0  64 
end; 
65 

66 

1502  67 
structure Tactical : TACTICAL = 
0  68 
struct 
69 

70 
(**** Tactics ****) 

71 

72 
(*A tactic maps a proof tree to a sequence of proof trees: 

73 
if length of sequence = 0 then the tactic does not apply; 

74 
if length > 1 then backtracking on the alternatives can occur.*) 

75 

1502  76 
type tactic = thm > thm Sequence.seq; 
0  77 

78 
(*Makes a tactic from one that uses the components of the state.*) 

1502  79 
fun STATE tacfun st = tacfun st st; 
0  80 

81 

82 
(*** LCFstyle tacticals ***) 

83 

84 
(*the tactical THEN performs one tactic followed by another*) 

1502  85 
fun (tac1 THEN tac2) st = Sequence.flats (Sequence.maps tac2 (tac1 st)); 
0  86 

87 

88 
(*The tactical ORELSE uses the first tactic that returns a nonempty sequence. 

89 
Like in LCF, ORELSE commits to either tac1 or tac2 immediately. 

90 
Does not backtrack to tac2 if tac1 was initially chosen. *) 

1502  91 
fun (tac1 ORELSE tac2) st = 
92 
case Sequence.pull(tac1 st) of 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

93 
None => tac2 st 
1502  94 
 sequencecell => Sequence.seqof(fn()=> sequencecell); 
0  95 

96 

97 
(*The tactical APPEND combines the results of two tactics. 

98 
Like ORELSE, but allows backtracking on both tac1 and tac2. 

99 
The tactic tac2 is not applied until needed.*) 

1502  100 
fun (tac1 APPEND tac2) st = 
101 
Sequence.append(tac1 st, 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

102 
Sequence.seqof(fn()=> Sequence.pull (tac2 st))); 
0  103 

104 
(*Like APPEND, but interleaves results of tac1 and tac2.*) 

1502  105 
fun (tac1 INTLEAVE tac2) st = 
106 
Sequence.interleave(tac1 st, 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

107 
Sequence.seqof(fn()=> Sequence.pull (tac2 st))); 
0  108 

671  109 
(*Conditional tactic. 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

110 
tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

111 
tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac) 
671  112 
*) 
1502  113 
fun (tac THEN_ELSE (tac1, tac2)) st = 
114 
case Sequence.pull(tac st) of 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

115 
None => tac2 st (*failed; try tactic 2*) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

116 
 seqcell => Sequence.flats (*succeeded; use tactic 1*) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

117 
(Sequence.maps tac1 (Sequence.seqof(fn()=> seqcell))); 
671  118 

119 

0  120 
(*Versions for combining tacticvalued functions, as in 
121 
SOMEGOAL (resolve_tac rls THEN' assume_tac) *) 

1502  122 
fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x; 
123 
fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x; 

124 
fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x; 

125 
fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x; 

0  126 

127 
(*passes all proofs through unchanged; identity of THEN*) 

1502  128 
fun all_tac st = Sequence.single st; 
0  129 

130 
(*passes no proofs through; identity of ORELSE and APPEND*) 

1502  131 
fun no_tac st = Sequence.null; 
0  132 

133 

134 
(*Make a tactic deterministic by chopping the tail of the proof sequence*) 

1502  135 
fun DETERM tac st = 
136 
case Sequence.pull (tac st) of 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

137 
None => Sequence.null 
1502  138 
 Some(x,_) => Sequence.cons(x, Sequence.null); 
0  139 

140 

141 
(*Conditional tactical: testfun controls which tactic to use next. 

142 
Beware: due to eager evaluation, both thentac and elsetac are evaluated.*) 

1502  143 
fun COND testfun thenf elsef = (fn prf => 
0  144 
if testfun prf then thenf prf else elsef prf); 
145 

146 
(*Do the tactic or else do nothing*) 

147 
fun TRY tac = tac ORELSE all_tac; 

148 

2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

149 
(*** Listoriented tactics ***) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

150 

85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

151 
local 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

152 
(*This version of EVERY avoids backtracking over repeated states*) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

153 

85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

154 
fun EVY (trail, []) st = 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

155 
Sequence.seqof (fn()=> Some(st, 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

156 
Sequence.seqof (fn()=> Sequence.pull (evyBack trail)))) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

157 
 EVY (trail, tac::tacs) st = 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

158 
case Sequence.pull(tac st) of 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

159 
None => evyBack trail (*failed: backtrack*) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

160 
 Some(st',q) => EVY ((st',q,tacs)::trail, tacs) st' 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

161 
and evyBack [] = Sequence.null (*no alternatives*) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

162 
 evyBack ((st',q,tacs)::trail) = 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

163 
case Sequence.pull q of 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

164 
None => evyBack trail 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

165 
 Some(st,q') => if eq_thm (st',st) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

166 
then evyBack ((st',q',tacs)::trail) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

167 
else EVY ((st,q',tacs)::trail, tacs) st 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

168 
in 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

169 

85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

170 
(* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

171 
fun EVERY tacs = EVY ([], tacs); 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

172 
end; 
2627  173 

0  174 

1502  175 
(* EVERY' [tac1,...,tacn] i equals tac1 i THEN ... THEN tacn i *) 
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

176 
fun EVERY' tacs i = EVERY (map (fn f => f i) tacs); 
0  177 

178 
(*Apply every tactic to 1*) 

1502  179 
fun EVERY1 tacs = EVERY' tacs 1; 
0  180 

181 
(* FIRST [tac1,...,tacn] equals tac1 ORELSE ... ORELSE tacn *) 

182 
fun FIRST tacs = foldr (op ORELSE) (tacs, no_tac); 

183 

1502  184 
(* FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i *) 
185 
fun FIRST' tacs = foldr (op ORELSE') (tacs, K no_tac); 

0  186 

187 
(*Apply first tactic to 1*) 

1502  188 
fun FIRST1 tacs = FIRST' tacs 1; 
0  189 

190 

191 
(*** Tracing tactics ***) 

192 

193 
(*Max number of goals to print  set by user*) 

194 
val goals_limit = ref 10; 

195 

196 
(*Print the current proof state and pass it on.*) 

1502  197 
val print_tac = 
198 
(fn st => 

199 
(!print_goals_ref (!goals_limit) st; Sequence.single st)); 

0  200 

201 
(*Pause until a line is typed  if nonempty then fail. *) 

1502  202 
fun pause_tac st = 
0  203 
(prs"** Press RETURN to continue: "; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

204 
if TextIO.inputLine TextIO.stdIn = "\n" then Sequence.single st 
1502  205 
else (prs"Goodbye\n"; Sequence.null)); 
0  206 

207 
exception TRACE_EXIT of thm 

208 
and TRACE_QUIT; 

209 

631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

210 
(*Tracing flags*) 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

211 
val trace_REPEAT= ref false 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

212 
and suppress_tracing = ref false; 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

213 

0  214 
(*Handle all tracing commands for current state and tactic *) 
1502  215 
fun exec_trace_command flag (tac, st) = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

216 
case TextIO.inputLine(TextIO.stdIn) of 
1502  217 
"\n" => tac st 
0  218 
 "f\n" => Sequence.null 
1502  219 
 "o\n" => (flag:=false; tac st) 
220 
 "s\n" => (suppress_tracing:=true; tac st) 

221 
 "x\n" => (prs"Exiting now\n"; raise (TRACE_EXIT st)) 

0  222 
 "quit\n" => raise TRACE_QUIT 
223 
 _ => (prs 

224 
"Type RETURN to continue or...\n\ 

225 
\ f  to fail here\n\ 

226 
\ o  to switch tracing off\n\ 

631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

227 
\ s  to suppress tracing until next entry to a tactical\n\ 
0  228 
\ x  to exit at this point\n\ 
229 
\ quit  to abort this tracing run\n\ 

1502  230 
\** Well? " ; exec_trace_command flag (tac, st)); 
0  231 

232 

233 
(*Extract from a tactic, a thm>thm seq function that handles tracing*) 

1502  234 
fun tracify flag tac st = 
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

235 
if !flag andalso not (!suppress_tracing) 
1502  236 
then (!print_goals_ref (!goals_limit) st; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

237 
prs"** Press RETURN to continue: "; 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

238 
exec_trace_command flag (tac,st)) 
1502  239 
else tac st; 
0  240 

241 
(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) 

1502  242 
fun traced_tac seqf st = 
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

243 
(suppress_tracing := false; 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

244 
Sequence.seqof (fn()=> seqf st 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

245 
handle TRACE_EXIT st' => Some(st', Sequence.null))); 
0  246 

247 

248 
(*Deterministic REPEAT: only retains the first outcome; 

703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

249 
uses less space than REPEAT; tail recursive. 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

250 
If nonnegative, n bounds the number of repetitions.*) 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

251 
fun REPEAT_DETERM_N n tac = 
1502  252 
let val tac = tracify trace_REPEAT tac 
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

253 
fun drep 0 st = Some(st, Sequence.null) 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

254 
 drep n st = 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

255 
(case Sequence.pull(tac st) of 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

256 
None => Some(st, Sequence.null) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

257 
 Some(st',_) => drep (n1) st') 
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

258 
in traced_tac (drep n) end; 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

259 

3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

260 
(*Allows any number of repetitions*) 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

261 
val REPEAT_DETERM = REPEAT_DETERM_N ~1; 
0  262 

263 
(*General REPEAT: maintains a stack of alternatives; tail recursive*) 

264 
fun REPEAT tac = 

1502  265 
let val tac = tracify trace_REPEAT tac 
0  266 
fun rep qs st = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

267 
case Sequence.pull(tac st) of 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

268 
None => Some(st, Sequence.seqof(fn()=> repq qs)) 
0  269 
 Some(st',q) => rep (q::qs) st' 
270 
and repq [] = None 

271 
 repq(q::qs) = case Sequence.pull q of 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

272 
None => repq qs 
0  273 
 Some(st,q) => rep (q::qs) st 
274 
in traced_tac (rep []) end; 

275 

276 
(*Repeat 1 or more times*) 

703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

277 
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; 
0  278 
fun REPEAT1 tac = tac THEN REPEAT tac; 
279 

280 

281 
(** Filtering tacticals **) 

282 

283 
(*Returns all states satisfying the predicate*) 

1502  284 
fun FILTER pred tac st = Sequence.filters pred (tac st); 
0  285 

286 
(*Returns all changed states*) 

1643
3f83b629f2e3
Fixed error in CHANGED (caused by variable renaming)
paulson
parents:
1583
diff
changeset

287 
fun CHANGED tac st = 
3f83b629f2e3
Fixed error in CHANGED (caused by variable renaming)
paulson
parents:
1583
diff
changeset

288 
let fun diff st' = not (eq_thm(st,st')) 
3f83b629f2e3
Fixed error in CHANGED (caused by variable renaming)
paulson
parents:
1583
diff
changeset

289 
in Sequence.filters diff (tac st) end; 
0  290 

291 

292 
(*** Tacticals based on subgoal numbering ***) 

293 

1502  294 
(*For n subgoals, performs tac(n) THEN ... THEN tac(1) 
295 
Essential to work backwards since tac(i) may add/delete subgoals at i. *) 

296 
fun ALLGOALS tac st = 

297 
let fun doall 0 = all_tac 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

298 
 doall n = tac(n) THEN doall(n1) 
1502  299 
in doall(nprems_of st)st end; 
0  300 

1502  301 
(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *) 
302 
fun SOMEGOAL tac st = 

303 
let fun find 0 = no_tac 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

304 
 find n = tac(n) ORELSE find(n1) 
1502  305 
in find(nprems_of st)st end; 
0  306 

1502  307 
(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n). 
0  308 
More appropriate than SOMEGOAL in some cases.*) 
1502  309 
fun FIRSTGOAL tac st = 
310 
let fun find (i,n) = if i>n then no_tac else tac(i) ORELSE find (i+1,n) 

311 
in find(1, nprems_of st)st end; 

0  312 

1502  313 
(*Repeatedly solve some using tac. *) 
314 
fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac)); 

315 
fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac)); 

0  316 

1502  317 
(*Repeatedly solve the first possible subgoal using tac. *) 
318 
fun REPEAT_FIRST tac = REPEAT1 (FIRSTGOAL (REPEAT1 o tac)); 

319 
fun REPEAT_DETERM_FIRST tac = REPEAT_DETERM1 (FIRSTGOAL (REPEAT_DETERM1 o tac)); 

0  320 

1502  321 
(*For n subgoals, tries to apply tac to n,...1 *) 
322 
fun TRYALL tac = ALLGOALS (TRY o tac); 

0  323 

324 

325 
(*Make a tactic for subgoal i, if there is one. *) 

2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2244
diff
changeset

326 
fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i1), i) st 
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2244
diff
changeset

327 
handle Subscript => Sequence.null; 
0  328 

2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

329 

a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

330 
(*** SELECT_GOAL ***) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

331 

0  332 
(*Tactical for restricting the effect of a tactic to subgoal i. 
1502  333 
Works by making a new state from subgoal i, applying tac to it, and 
0  334 
composing the resulting metathm with the original state. 
335 
The "main goal" of the new state will not be atomic, some tactics may fail! 

336 
DOES NOT work if tactic affects the main goal other than by instantiation.*) 

337 

2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

338 
(*SELECT_GOAL optimization: replace the conclusion by a variable X, 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

339 
to avoid copying. Proof states have X==concl as an assuption.*) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

340 

a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

341 
val prop_equals = cterm_of Sign.proto_pure 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

342 
(Const("==", propT>propT>propT)); 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

343 

a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

344 
fun mk_prop_equals(t,u) = capply (capply prop_equals t) u; 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

345 

a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

346 
(*Like trivial but returns [ct==X] ct==>X instead of ct==>ct, if possible. 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

347 
It is paired with a function to undo the transformation. If ct contains 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

348 
Vars then it returns ct==>ct.*) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

349 
fun eq_trivial ct = 
2807
04c080e60f31
A more explicit prefix because gensym now generates easily predicatable
paulson
parents:
2672
diff
changeset

350 
let val xfree = cterm_of Sign.proto_pure (Free (gensym"EQ_TRIVIAL_", propT)) 
2158
77dfe65b5bb3
Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes
paulson
parents:
2005
diff
changeset

351 
val ct_eq_x = mk_prop_equals (ct, xfree) 
2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

352 
and refl_ct = reflexive ct 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

353 
fun restore th = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

354 
implies_elim 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

355 
(forall_elim ct (forall_intr xfree (implies_intr ct_eq_x th))) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

356 
refl_ct 
2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

357 
in (equal_elim 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

358 
(combination (combination refl_implies refl_ct) (assume ct_eq_x)) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

359 
(trivial ct), 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

360 
restore) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

361 
end (*Fails if there are Vars or TVars*) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

362 
handle THM _ => (trivial ct, I); 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

363 

a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

364 
(*Does the work of SELECT_GOAL. *) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

365 
fun select tac st0 i = 
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2244
diff
changeset

366 
let val (eq_cprem, restore) = (*we hope maxidx goes to ~1*) 
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2244
diff
changeset

367 
eq_trivial (adjust_maxidx (List.nth(cprems_of st0, i1))) 
2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

368 
fun next st = bicompose false (false, restore st, nprems_of st) i st0 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

369 
in Sequence.flats (Sequence.maps next (tac eq_cprem)) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

370 
end; 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

371 

2158
77dfe65b5bb3
Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes
paulson
parents:
2005
diff
changeset

372 
(* (!!selct. PROP ?V) ==> PROP ?V ; contains NO TYPE VARIABLES.*) 
0  373 
val dummy_quant_rl = 
2158
77dfe65b5bb3
Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes
paulson
parents:
2005
diff
changeset

374 
read_cterm Sign.proto_pure ("!!selct::prop. PROP V",propT) > 
77dfe65b5bb3
Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes
paulson
parents:
2005
diff
changeset

375 
assume > forall_elim_var 0 > standard; 
0  376 

377 
(* Prevent the subgoal's assumptions from becoming additional subgoals in the 

378 
new proof state by enclosing them by a universal quantification *) 

1502  379 
fun protect_subgoal st i = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

380 
Sequence.hd (bicompose false (false,dummy_quant_rl,1) i st) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

381 
handle _ => error"SELECT_GOAL  impossible error???"; 
0  382 

1502  383 
fun SELECT_GOAL tac i st = 
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2244
diff
changeset

384 
case (i, List.drop(prems_of st, i1)) of 
0  385 
(_,[]) => Sequence.null 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

386 
 (1,[_]) => tac st (*If i=1 and only one subgoal do nothing!*) 
1502  387 
 (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i 
388 
 (_, _::_) => select tac st i; 

0  389 

390 

391 
(*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) 

392 
H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. 

393 
Main difference from strip_assums concerns parameters: 

394 
it replaces the bound variables by free variables. *) 

395 
fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

396 
strip_context_aux (params, H::Hs, B) 
0  397 
 strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) = 
398 
let val (b,u) = variant_abs(a,T,t) 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

399 
in strip_context_aux ((b,T)::params, Hs, u) end 
0  400 
 strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); 
401 

402 
fun strip_context A = strip_context_aux ([],[],A); 

403 

404 

405 
(**** METAHYPS  tactical for using hypotheses as metalevel assumptions 

1502  406 
METAHYPS (fn prems => tac prems) i 
0  407 

408 
converts subgoal i, of the form !!x1...xm. [ A1;...;An] ==> A into a new 

409 
proof state A==>A, supplying A1,...,An as metalevel assumptions (in 

410 
"prems"). The parameters x1,...,xm become free variables. If the 

411 
resulting proof state is [ B1;...;Bk] ==> C (possibly assuming A1,...,An) 

412 
then it is lifted back into the original context, yielding k subgoals. 

413 

414 
Replaces unknowns in the context by Frees having the prefix METAHYP_ 

415 
New unknowns in [ B1;...;Bk] ==> C are lifted over x1,...,xm. 

416 
DOES NOT HANDLE TYPE UNKNOWNS. 

417 
****) 

418 

419 
local 

420 

421 
(*Lefttoright replacements: ctpairs = [...,(vi,ti),...]. 

422 
Instantiates distinct free variables by terms of same type.*) 

423 
fun free_instantiate ctpairs = 

424 
forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); 

425 

426 
fun free_of s ((a,i), T) = 

427 
Free(s ^ (case i of 0 => a  _ => a ^ "_" ^ string_of_int i), 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

428 
T) 
0  429 

430 
fun mk_inst (var as Var(v,T)) = (var, free_of "METAHYP1_" (v,T)) 

431 
in 

432 

1502  433 
fun metahyps_aux_tac tacf (prem,i) state = 
0  434 
let val {sign,maxidx,...} = rep_thm state 
230  435 
val cterm = cterm_of sign 
0  436 
(*find all vars in the hyps  should find tvars also!*) 
1502  437 
val hyps_vars = foldr add_term_vars (Logic.strip_assums_hyp prem, []) 
0  438 
val insts = map mk_inst hyps_vars 
439 
(*replace the hyps_vars by Frees*) 

440 
val prem' = subst_atomic insts prem 

441 
val (params,hyps,concl) = strip_context prem' 

442 
val fparams = map Free params 

443 
val cparams = map cterm fparams 

444 
and chyps = map cterm hyps 

445 
val hypths = map assume chyps 

446 
fun swap_ctpair (t,u) = (cterm u, cterm t) 

447 
(*Subgoal variables: make Free; lift type over params*) 

448 
fun mk_subgoal_inst concl_vars (var as Var(v,T)) = 

449 
if var mem concl_vars 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

450 
then (var, true, free_of "METAHYP2_" (v,T)) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

451 
else (var, false, 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

452 
free_of "METAHYP2_" (v, map #2 params >T)) 
0  453 
(*Instantiate subgoal vars by Free applied to params*) 
454 
fun mk_ctpair (t,in_concl,u) = 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

455 
if in_concl then (cterm t, cterm u) 
0  456 
else (cterm t, cterm (list_comb (u,fparams))) 
457 
(*Restore Vars with higher type and index*) 

458 
fun mk_subgoal_swap_ctpair 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

459 
(t as Var((a,i),_), in_concl, u as Free(_,U)) = 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

460 
if in_concl then (cterm u, cterm t) 
0  461 
else (cterm u, cterm(Var((a, i+maxidx), U))) 
462 
(*Embed B in the original context of params and hyps*) 

1502  463 
fun embed B = list_all_free (params, Logic.list_implies (hyps, B)) 
0  464 
(*Strip the context using elimination rules*) 
465 
fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths 

466 
(*Embed an ff pair in the original params*) 

1502  467 
fun embed_ff(t,u) = Logic.mk_flexpair (list_abs_free (params, t), 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

468 
list_abs_free (params, u)) 
0  469 
(*Remove parameter abstractions from the ff pairs*) 
470 
fun elim_ff ff = flexpair_abs_elim_list cparams ff 

471 
(*A form of lifting that discharges assumptions.*) 

472 
fun relift st = 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

473 
let val prop = #prop(rep_thm st) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

474 
val subgoal_vars = (*Vars introduced in the subgoals*) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

475 
foldr add_term_vars (Logic.strip_imp_prems prop, []) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

476 
and concl_vars = add_term_vars (Logic.strip_imp_concl prop, []) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

477 
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

478 
val st' = instantiate ([], map mk_ctpair subgoal_insts) st 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

479 
val emBs = map (cterm o embed) (prems_of st') 
0  480 
and ffs = map (cterm o embed_ff) (tpairs_of st') 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

481 
val Cth = implies_elim_list st' 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

482 
(map (elim_ff o assume) ffs @ 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

483 
map (elim o assume) emBs) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

484 
in (*restore the unknowns to the hypotheses*) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

485 
free_instantiate (map swap_ctpair insts @ 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

486 
map mk_subgoal_swap_ctpair subgoal_insts) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

487 
(*discharge assumptions from state in same order*) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

488 
(implies_intr_list (ffs@emBs) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

489 
(forall_intr_list cparams (implies_intr_list chyps Cth))) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

490 
end 
0  491 
val subprems = map (forall_elim_vars 0) hypths 
492 
and st0 = trivial (cterm concl) 

493 
(*function to replace the current subgoal*) 

494 
fun next st = bicompose false (false, relift st, nprems_of st) 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

495 
i state 
1502  496 
in Sequence.flats (Sequence.maps next (tacf subprems st0)) 
497 
end; 

0  498 
end; 
499 

500 
fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf); 

501 

502 
end; 

1502  503 

504 
open Tactical; 