author  paulson 
Fri, 16 Feb 1996 12:57:32 +0100  
changeset 1502  b612093c8bff 
parent 1460  5a6f2aabd538 
child 1583  bc902840aab5 
permissions  rwrr 
1460  1 
(* Title: tctical 
0  2 
ID: $Id$ 
1460  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

6 
Tacticals 

7 
*) 

8 

9 
infix 1 THEN THEN' THEN_BEST_FIRST; 

10 
infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE'; 

11 

671  12 
infix 0 THEN_ELSE; 
13 

0  14 

15 
signature TACTICAL = 

16 
sig 

1502  17 
type tactic (* = thm > thm Sequence.seq*) 
1460  18 
val all_tac : tactic 
19 
val ALLGOALS : (int > tactic) > tactic 

20 
val APPEND : tactic * tactic > tactic 

21 
val APPEND' : ('a > tactic) * ('a > tactic) > 'a > tactic 

22 
val BEST_FIRST : (thm > bool) * (thm > int) > tactic > tactic 

23 
val BREADTH_FIRST : (thm > bool) > tactic > tactic 

24 
val CHANGED : tactic > tactic 

25 
val COND : (thm > bool) > tactic > tactic > tactic 

26 
val DEPTH_FIRST : (thm > bool) > tactic > tactic 

27 
val DEPTH_SOLVE : tactic > tactic 

28 
val DEPTH_SOLVE_1 : tactic > tactic 

29 
val DETERM : tactic > tactic 

30 
val EVERY : tactic list > tactic 

31 
val EVERY' : ('a > tactic) list > 'a > tactic 

32 
val EVERY1 : (int > tactic) list > tactic 

33 
val FILTER : (thm > bool) > tactic > tactic 

34 
val FIRST : tactic list > tactic 

35 
val FIRST' : ('a > tactic) list > 'a > tactic 

36 
val FIRST1 : (int > tactic) list > tactic 

37 
val FIRSTGOAL : (int > tactic) > tactic 

38 
val goals_limit : int ref 

39 
val has_fewer_prems : int > thm > bool 

40 
val IF_UNSOLVED : tactic > tactic 

41 
val INTLEAVE : tactic * tactic > tactic 

42 
val INTLEAVE' : ('a > tactic) * ('a > tactic) > 'a > tactic 

43 
val METAHYPS : (thm list > tactic) > int > tactic 

44 
val no_tac : tactic 

45 
val ORELSE : tactic * tactic > tactic 

46 
val ORELSE' : ('a > tactic) * ('a > tactic) > 'a > tactic 

47 
val pause_tac : tactic 

48 
val print_tac : tactic 

49 
val REPEAT : tactic > tactic 

50 
val REPEAT1 : tactic > tactic 

51 
val REPEAT_DETERM_N : int > tactic > tactic 

52 
val REPEAT_DETERM : tactic > tactic 

53 
val REPEAT_DETERM1 : tactic > tactic 

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

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

55 
val REPEAT_DETERM_SOME: (int > tactic) > tactic 
1460  56 
val REPEAT_FIRST : (int > tactic) > tactic 
57 
val REPEAT_SOME : (int > tactic) > tactic 

58 
val SELECT_GOAL : tactic > int > tactic 

59 
val SOMEGOAL : (int > tactic) > tactic 

60 
val STATE : (thm > tactic) > tactic 

61 
val strip_context : term > (string * typ) list * term list * term 

62 
val SUBGOAL : ((term*int) > tactic) > int > tactic 

63 
val suppress_tracing : bool ref 

64 
val THEN : tactic * tactic > tactic 

65 
val THEN' : ('a > tactic) * ('a > tactic) > 'a > tactic 

66 
val THEN_BEST_FIRST : tactic * ((thm>bool) * (thm>int) * tactic) 

67 
> tactic 

68 
val THEN_ELSE : tactic * (tactic*tactic) > tactic 

69 
val traced_tac : (thm > (thm * thm Sequence.seq) option) > tactic 

70 
val tracify : bool ref > tactic > thm > thm Sequence.seq 

71 
val trace_BEST_FIRST : bool ref 

72 
val trace_DEPTH_FIRST : bool ref 

73 
val trace_REPEAT : bool ref 

74 
val TRY : tactic > tactic 

75 
val TRYALL : (int > tactic) > tactic 

0  76 
end; 
77 

78 

1502  79 
structure Tactical : TACTICAL = 
0  80 
struct 
81 

82 
(**** Tactics ****) 

83 

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

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

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

87 

1502  88 
type tactic = thm > thm Sequence.seq; 
0  89 

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

1502  91 
fun STATE tacfun st = tacfun st st; 
0  92 

93 

94 
(*** LCFstyle tacticals ***) 

95 

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

1502  97 
fun (tac1 THEN tac2) st = Sequence.flats (Sequence.maps tac2 (tac1 st)); 
0  98 

99 

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

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

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

1502  103 
fun (tac1 ORELSE tac2) st = 
104 
case Sequence.pull(tac1 st) of 

105 
None => tac2 st 

106 
 sequencecell => Sequence.seqof(fn()=> sequencecell); 

0  107 

108 

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

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

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

1502  112 
fun (tac1 APPEND tac2) st = 
113 
Sequence.append(tac1 st, 

114 
Sequence.seqof(fn()=> Sequence.pull (tac2 st))); 

0  115 

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

1502  117 
fun (tac1 INTLEAVE tac2) st = 
118 
Sequence.interleave(tac1 st, 

119 
Sequence.seqof(fn()=> Sequence.pull (tac2 st))); 

0  120 

671  121 
(*Conditional tactic. 
1460  122 
tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2) 
123 
tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac) 

671  124 
*) 
1502  125 
fun (tac THEN_ELSE (tac1, tac2)) st = 
126 
case Sequence.pull(tac st) of 

127 
None => tac2 st (*failed; try tactic 2*) 

1460  128 
 seqcell => Sequence.flats (*succeeded; use tactic 1*) 
1502  129 
(Sequence.maps tac1 (Sequence.seqof(fn()=> seqcell))); 
671  130 

131 

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

1502  134 
fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x; 
135 
fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x; 

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

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

0  138 

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

1502  140 
fun all_tac st = Sequence.single st; 
0  141 

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

1502  143 
fun no_tac st = Sequence.null; 
0  144 

145 

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

1502  147 
fun DETERM tac st = 
148 
case Sequence.pull (tac st) of 

1460  149 
None => Sequence.null 
1502  150 
 Some(x,_) => Sequence.cons(x, Sequence.null); 
0  151 

152 

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

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

1502  155 
fun COND testfun thenf elsef = (fn prf => 
0  156 
if testfun prf then thenf prf else elsef prf); 
157 

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

159 
fun TRY tac = tac ORELSE all_tac; 

160 

161 

162 
(*** Listoriented tactics ***) 

163 

164 
(* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *) 

165 
fun EVERY tacs = foldr (op THEN) (tacs, all_tac); 

166 

1502  167 
(* EVERY' [tac1,...,tacn] i equals tac1 i THEN ... THEN tacn i *) 
168 
fun EVERY' tacs = foldr (op THEN') (tacs, K all_tac); 

0  169 

170 
(*Apply every tactic to 1*) 

1502  171 
fun EVERY1 tacs = EVERY' tacs 1; 
0  172 

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

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

175 

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

0  178 

179 
(*Apply first tactic to 1*) 

1502  180 
fun FIRST1 tacs = FIRST' tacs 1; 
0  181 

182 

183 
(*** Tracing tactics ***) 

184 

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

186 
val goals_limit = ref 10; 

187 

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

1502  189 
val print_tac = 
190 
(fn st => 

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

0  192 

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

1502  194 
fun pause_tac st = 
0  195 
(prs"** Press RETURN to continue: "; 
1502  196 
if input(std_in,1) = "\n" then Sequence.single st 
197 
else (prs"Goodbye\n"; Sequence.null)); 

0  198 

199 
exception TRACE_EXIT of thm 

200 
and TRACE_QUIT; 

201 

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

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

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

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

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

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

207 

0  208 
(*Handle all tracing commands for current state and tactic *) 
1502  209 
fun exec_trace_command flag (tac, st) = 
0  210 
case input_line(std_in) of 
1502  211 
"\n" => tac st 
0  212 
 "f\n" => Sequence.null 
1502  213 
 "o\n" => (flag:=false; tac st) 
214 
 "s\n" => (suppress_tracing:=true; tac st) 

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

0  216 
 "quit\n" => raise TRACE_QUIT 
217 
 _ => (prs 

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

219 
\ f  to fail here\n\ 

220 
\ 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

221 
\ s  to suppress tracing until next entry to a tactical\n\ 
0  222 
\ x  to exit at this point\n\ 
223 
\ quit  to abort this tracing run\n\ 

1502  224 
\** Well? " ; exec_trace_command flag (tac, st)); 
0  225 

226 

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

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

229 
if !flag andalso not (!suppress_tracing) 
1502  230 
then (!print_goals_ref (!goals_limit) st; 
1460  231 
prs"** Press RETURN to continue: "; 
1502  232 
exec_trace_command flag (tac,st)) 
233 
else tac st; 

0  234 

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

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

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

238 
Sequence.seqof (fn()=> seqf st 
1502  239 
handle TRACE_EXIT st' => Some(st', Sequence.null))); 
0  240 

241 

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

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

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

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

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

247 
fun drep 0 st = Some(st, Sequence.null) 
1460  248 
 drep n st = 
1502  249 
(case Sequence.pull(tac st) of 
1460  250 
None => Some(st, Sequence.null) 
251 
 Some(st',_) => drep (n1) st') 

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

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

253 

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

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

255 
val REPEAT_DETERM = REPEAT_DETERM_N ~1; 
0  256 

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

258 
fun REPEAT tac = 

1502  259 
let val tac = tracify trace_REPEAT tac 
0  260 
fun rep qs st = 
1502  261 
case Sequence.pull(tac st) of 
1460  262 
None => Some(st, Sequence.seqof(fn()=> repq qs)) 
0  263 
 Some(st',q) => rep (q::qs) st' 
264 
and repq [] = None 

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

1460  266 
None => repq qs 
0  267 
 Some(st,q) => rep (q::qs) st 
268 
in traced_tac (rep []) end; 

269 

270 
(*Repeat 1 or more times*) 

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

271 
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; 
0  272 
fun REPEAT1 tac = tac THEN REPEAT tac; 
273 

274 

275 
(** Search tacticals **) 

276 

729
cc4c4eafe628
Pure/tctical/protect_subgoal: simplified to use Sequence.hd
lcp
parents:
709
diff
changeset

277 
(*Searches until "satp" reports proof tree as satisfied. 
cc4c4eafe628
Pure/tctical/protect_subgoal: simplified to use Sequence.hd
lcp
parents:
709
diff
changeset

278 
Suppresses duplicate solutions to minimize search space.*) 
0  279 
fun DEPTH_FIRST satp tac = 
1502  280 
let val tac = tracify trace_DEPTH_FIRST tac 
729
cc4c4eafe628
Pure/tctical/protect_subgoal: simplified to use Sequence.hd
lcp
parents:
709
diff
changeset

281 
fun depth used [] = None 
cc4c4eafe628
Pure/tctical/protect_subgoal: simplified to use Sequence.hd
lcp
parents:
709
diff
changeset

282 
 depth used (q::qs) = 
1460  283 
case Sequence.pull q of 
284 
None => depth used qs 

285 
 Some(st,stq) => 

286 
if satp st andalso not (gen_mem eq_thm (st, used)) 

287 
then Some(st, Sequence.seqof 

288 
(fn()=> depth (st::used) (stq::qs))) 

1502  289 
else depth used (tac st :: stq :: qs) 
729
cc4c4eafe628
Pure/tctical/protect_subgoal: simplified to use Sequence.hd
lcp
parents:
709
diff
changeset

290 
in traced_tac (fn st => depth [] ([Sequence.single st])) end; 
cc4c4eafe628
Pure/tctical/protect_subgoal: simplified to use Sequence.hd
lcp
parents:
709
diff
changeset

291 

0  292 

293 

294 
(*Predicate: Does the rule have fewer than n premises?*) 

295 
fun has_fewer_prems n rule = (nprems_of rule < n); 

296 

297 
(*Apply a tactic if subgoals remain, else do nothing.*) 

298 
val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; 

299 

300 
(*Tactical to reduce the number of premises by 1. 

301 
If no subgoals then it must fail! *) 

302 
fun DEPTH_SOLVE_1 tac = STATE 

1502  303 
(fn st => 
304 
(case nprems_of st of 

1460  305 
0 => no_tac 
0  306 
 n => DEPTH_FIRST (has_fewer_prems n) tac)); 
307 

308 
(*Uses depthfirst search to solve ALL subgoals*) 

309 
val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1); 

310 

311 
(*** Bestfirst search ***) 

312 

313 
(*Insertion into priority queue of states *) 

314 
fun insert (nth: int*thm, []) = [nth] 

315 
 insert ((m,th), (n,th')::nths) = 

316 
if n<m then (n,th') :: insert ((m,th), nths) 

317 
else if n=m andalso eq_thm(th,th') 

318 
then (n,th')::nths 

319 
else (m,th)::(n,th')::nths; 

320 

321 
(*For creating output sequence*) 

322 
fun some_of_list [] = None 

323 
 some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l)); 

324 

325 

326 
(* Bestfirst search for a state that satisfies satp (incl initial state) 

327 
Function sizef estimates size of problem remaining (smaller means better). 

1502  328 
tactic tac0 sets up the initial priority queue, which is searched by tac. *) 
329 
fun tac0 THEN_BEST_FIRST (satp, sizef, tac1) = 

330 
let val tac = tracify trace_BEST_FIRST tac1 

0  331 
fun pairsize th = (sizef th, th); 
332 
fun bfs (news,nprfs) = 

1460  333 
(case partition satp news of 
334 
([],nonsats) => next(foldr insert 

335 
(map pairsize nonsats, nprfs)) 

336 
 (sats,_) => some_of_list sats) 

0  337 
and next [] = None 
338 
 next ((n,prf)::nprfs) = 

1460  339 
(if !trace_BEST_FIRST 
340 
then writeln("state size = " ^ string_of_int n ^ 

341 
" queue length =" ^ string_of_int (length nprfs)) 

0  342 
else (); 
1502  343 
bfs (Sequence.list_of_s (tac prf), nprfs)) 
344 
fun btac st = bfs (Sequence.list_of_s (tac0 st), []) 

345 
in traced_tac btac end; 

0  346 

347 
(*Ordinary bestfirst search, with no initial tactic*) 

348 
fun BEST_FIRST (satp,sizef) tac = all_tac THEN_BEST_FIRST (satp,sizef,tac); 

349 

350 
(*Breadthfirst search to satisfy satpred (including initial state) 

351 
SLOW  SHOULD NOT USE APPEND!*) 

1502  352 
fun BREADTH_FIRST satpred tac = 
353 
let val tacf = Sequence.list_of_s o tac; 

0  354 
fun bfs prfs = 
1460  355 
(case partition satpred prfs of 
356 
([],[]) => [] 

357 
 ([],nonsats) => 

358 
(prs("breadth=" ^ string_of_int(length nonsats) ^ "\n"); 

359 
bfs (flat (map tacf nonsats))) 

360 
 (sats,_) => sats) 

1502  361 
in (fn st => Sequence.s_of_list (bfs [st])) end; 
0  362 

363 

364 
(** Filtering tacticals **) 

365 

366 
(*Returns all states satisfying the predicate*) 

1502  367 
fun FILTER pred tac st = Sequence.filters pred (tac st); 
0  368 

369 
(*Returns all changed states*) 

1502  370 
fun CHANGED tac = 
371 
(fn st => 

372 
let fun diff st = not (eq_thm(st,st)) 

373 
in Sequence.filters diff (tac st) 

0  374 
end ); 
375 

376 

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

378 

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

381 
fun ALLGOALS tac st = 

382 
let fun doall 0 = all_tac 

383 
 doall n = tac(n) THEN doall(n1) 

384 
in doall(nprems_of st)st end; 

0  385 

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

388 
let fun find 0 = no_tac 

389 
 find n = tac(n) ORELSE find(n1) 

390 
in find(nprems_of st)st end; 

0  391 

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

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

0  397 

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

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

0  401 

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

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

0  405 

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

0  408 

409 

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

1502  411 
fun SUBGOAL goalfun i st = 
412 
case drop(i1, prems_of st) of 

0  413 
[] => Sequence.null 
1502  414 
 prem::_ => goalfun (prem,i) st; 
0  415 

416 
(*Tactical for restricting the effect of a tactic to subgoal i. 

1502  417 
Works by making a new state from subgoal i, applying tac to it, and 
0  418 
composing the resulting metathm with the original state. 
419 
The "main goal" of the new state will not be atomic, some tactics may fail! 

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

421 

31
eb01df4ffe66
tctical/dummy_quant_rl: specifies type prop to avoid the type variable
lcp
parents:
0
diff
changeset

422 
(* (!!x. PROP ?V) ==> PROP ?V ; contains NO TYPE VARIABLES.*) 
0  423 
val dummy_quant_rl = 
424 
standard (forall_elim_var 0 (assume 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
729
diff
changeset

425 
(read_cterm Sign.proto_pure ("!!x::prop. PROP V",propT)))); 
0  426 

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

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

1502  429 
fun protect_subgoal st i = 
430 
Sequence.hd (bicompose false (false,dummy_quant_rl,1) i st) 

1460  431 
handle _ => error"SELECT_GOAL  impossible error???"; 
0  432 

433 
(*Does the work of SELECT_GOAL. *) 

1502  434 
fun select tac st0 i = 
435 
let val cprem::_ = drop(i1, cprems_of st0) 

436 
fun next st = bicompose false (false, st, nprems_of st) i st0 

437 
in Sequence.flats (Sequence.maps next (tac (trivial cprem))) 

0  438 
end; 
439 

1502  440 
fun SELECT_GOAL tac i st = 
441 
case (i, drop(i1, prems_of st)) of 

0  442 
(_,[]) => Sequence.null 
1502  443 
 (1,[_]) => tac st (*If i=1 and only one subgoal do nothing!*) 
444 
 (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i 

445 
 (_, _::_) => select tac st i; 

0  446 

447 

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

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

450 
Main difference from strip_assums concerns parameters: 

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

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

1460  453 
strip_context_aux (params, H::Hs, B) 
0  454 
 strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) = 
455 
let val (b,u) = variant_abs(a,T,t) 

1460  456 
in strip_context_aux ((b,T)::params, Hs, u) end 
0  457 
 strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); 
458 

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

460 

461 

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

1502  463 
METAHYPS (fn prems => tac prems) i 
0  464 

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

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

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

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

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

470 

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

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

473 
DOES NOT HANDLE TYPE UNKNOWNS. 

474 
****) 

475 

476 
local 

477 

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

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

480 
fun free_instantiate ctpairs = 

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

482 

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

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

1460  485 
T) 
0  486 

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

488 
in 

489 

1502  490 
fun metahyps_aux_tac tacf (prem,i) state = 
0  491 
let val {sign,maxidx,...} = rep_thm state 
230  492 
val cterm = cterm_of sign 
0  493 
(*find all vars in the hyps  should find tvars also!*) 
1502  494 
val hyps_vars = foldr add_term_vars (Logic.strip_assums_hyp prem, []) 
0  495 
val insts = map mk_inst hyps_vars 
496 
(*replace the hyps_vars by Frees*) 

497 
val prem' = subst_atomic insts prem 

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

499 
val fparams = map Free params 

500 
val cparams = map cterm fparams 

501 
and chyps = map cterm hyps 

502 
val hypths = map assume chyps 

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

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

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

506 
if var mem concl_vars 

1460  507 
then (var, true, free_of "METAHYP2_" (v,T)) 
508 
else (var, false, 

509 
free_of "METAHYP2_" (v, map #2 params >T)) 

0  510 
(*Instantiate subgoal vars by Free applied to params*) 
511 
fun mk_ctpair (t,in_concl,u) = 

1460  512 
if in_concl then (cterm t, cterm u) 
0  513 
else (cterm t, cterm (list_comb (u,fparams))) 
514 
(*Restore Vars with higher type and index*) 

515 
fun mk_subgoal_swap_ctpair 

1460  516 
(t as Var((a,i),_), in_concl, u as Free(_,U)) = 
517 
if in_concl then (cterm u, cterm t) 

0  518 
else (cterm u, cterm(Var((a, i+maxidx), U))) 
519 
(*Embed B in the original context of params and hyps*) 

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

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

1502  524 
fun embed_ff(t,u) = Logic.mk_flexpair (list_abs_free (params, t), 
525 
list_abs_free (params, u)) 

0  526 
(*Remove parameter abstractions from the ff pairs*) 
527 
fun elim_ff ff = flexpair_abs_elim_list cparams ff 

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

529 
fun relift st = 

1460  530 
let val prop = #prop(rep_thm st) 
531 
val subgoal_vars = (*Vars introduced in the subgoals*) 

1502  532 
foldr add_term_vars (Logic.strip_imp_prems prop, []) 
533 
and concl_vars = add_term_vars (Logic.strip_imp_concl prop, []) 

1460  534 
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars 
535 
val st' = instantiate ([], map mk_ctpair subgoal_insts) st 

536 
val emBs = map (cterm o embed) (prems_of st') 

0  537 
and ffs = map (cterm o embed_ff) (tpairs_of st') 
1460  538 
val Cth = implies_elim_list st' 
539 
(map (elim_ff o assume) ffs @ 

540 
map (elim o assume) emBs) 

541 
in (*restore the unknowns to the hypotheses*) 

542 
free_instantiate (map swap_ctpair insts @ 

543 
map mk_subgoal_swap_ctpair subgoal_insts) 

544 
(*discharge assumptions from state in same order*) 

545 
(implies_intr_list (ffs@emBs) 

546 
(forall_intr_list cparams (implies_intr_list chyps Cth))) 

547 
end 

0  548 
val subprems = map (forall_elim_vars 0) hypths 
549 
and st0 = trivial (cterm concl) 

550 
(*function to replace the current subgoal*) 

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

1460  552 
i state 
1502  553 
in Sequence.flats (Sequence.maps next (tacf subprems st0)) 
554 
end; 

0  555 
end; 
556 

557 
fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf); 

558 

559 
end; 

1502  560 

561 
open Tactical; 